:: FILTER_2 semantic presentation

for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )

proof end;

theorem :: FILTER_2:2

for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d' being Element of S st g = f || S & d' = d holds
( ( d is_a_left_unity_wrt f implies d' is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d' is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d' is_a_unity_wrt g ) )

proof end;

theorem Th3: :: FILTER_2:3

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )

proof end;

theorem :: FILTER_2:4

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2

proof end;

theorem Th5: :: FILTER_2:5

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2

proof end;

definition

let D be non empty set ;
let X1, X2 be Subset of D;
:: original: =
redefine pred X1 = X2 means :: FILTER_2:def 1
for x being Element of D holds
( x in X1 iff x in X2 );
compatibility by SUBSET_1:8;

end;

:: deftheorem defines = FILTER_2:def 1 :

deffunc H₁( LattStr ) -> set = the carrier of $1;

deffunc H₂( LattStr ) -> Relation of [:the carrier of $1,the carrier of $1:],the carrier of $1 = the L_join of $1;

deffunc H₃( LattStr ) -> Relation of [:the carrier of $1,the carrier of $1:],the carrier of $1 = the L_meet of $1;

theorem :: FILTER_2:6

for L1, L2 being LattStr st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
L1 .: = L2 .: ;

theorem :: FILTER_2:7

for L being Lattice holds (L .: ) .: = LattStr(# the carrier of L,the L_join of L,the L_meet of L #) ;

theorem :: FILTER_2:8

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )

proof end;

theorem Th9: :: FILTER_2:9

for L1, L2 being 0_Lattice st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
Bottom L1 = Bottom L2

proof end;

theorem Th10: :: FILTER_2:10

for L1, L2 being 1_Lattice st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
Top L1 = Top L2

proof end;

theorem Th11: :: FILTER_2:11

for L1, L2 being C_Lattice st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2

proof end;

theorem :: FILTER_2:12

for L1, L2 being B_Lattice st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `

proof end;

theorem :: FILTER_2:13

for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L

proof end;

theorem Th14: :: FILTER_2:14

for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is ClosedSubset of L

proof end;

definition

let L be Lattice;
:: original: Filter
redefine mode Filter of L -> non empty ClosedSubset of L;
coherence by LATTICE4:11;

end;

definition

let L be Lattice;
:: original: <.
redefine func <.L.) -> Filter of L;
coherence ;
let p be Element of L;
:: original: <.
redefine func <.p.) -> Filter of L;
coherence ;

end;

definition

let L be Lattice;
let D be non empty Subset of L;
:: original: <.
redefine func <.D.) -> Filter of L;
coherence ;

end;

definition

let L be D_Lattice;
let F1, F2 be Filter of L;
:: original: "/\"
redefine func F1 "/\" F2 -> Filter of L;
coherence

proof end;

end;

definition

let L be Lattice;
canceled;
mode Ideal of L -> non empty ClosedSubset of L means :Def3: :: FILTER_2:def 3
for p, q being Element of L holds
( ( p in it & q in it ) iff p "\/" q in it );
existence

proof end;

end;

:: deftheorem FILTER_2:def 2 :

:: deftheorem Def3 defines Ideal FILTER_2:def 3 :

theorem Th15: :: FILTER_2:15

for L being Lattice
for X being non empty Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is Ideal of L

proof end;

theorem Th16: :: FILTER_2:16

for L1, L2 being Lattice st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for x being set st x is Filter of L1 holds
x is Filter of L2

proof end;

theorem Th17: :: FILTER_2:17

proof end;

definition

let L be Lattice;
let p be Element of L;
func p .: -> Element of (L .: ) equals :: FILTER_2:def 4
p;
coherence ;

end;

:: deftheorem defines .: FILTER_2:def 4 :

definition

let L be Lattice;
let p be Element of (L .: );
func .: p -> Element of L equals :: FILTER_2:def 5
p;
coherence ;

end;

:: deftheorem defines .: FILTER_2:def 5 :

theorem :: FILTER_2:18

for L being Lattice
for p being Element of L
for p' being Element of (L .: ) holds
( .: (p .: ) = p & (.: p') .: = p' ) ;

theorem :: FILTER_2:19

for L being Lattice
for p, q being Element of L
for p', q' being Element of (L .: ) holds
( p "/\" q = (p .: ) "\/" (q .: ) & p "\/" q = (p .: ) "/\" (q .: ) & p' "/\" q' = (.: p') "\/" (.: q') & p' "\/" q' = (.: p') "/\" (.: q') ) ;

theorem Th20: :: FILTER_2:20

for L being Lattice
for p, q being Element of L
for p', q' being Element of (L .: ) holds
( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p' [= q' implies .: q' [= .: p' ) & ( .: q' [= .: p' implies p' [= q' ) ) by LATTICE2:53, LATTICE2:54;

theorem Th21: :: FILTER_2:21

for L being Lattice
for x being set holds
( x is Ideal of L iff x is Filter of L .: )

proof end;

definition

let L be Lattice;
let X be Subset of L;
func X .: -> Subset of (L .: ) equals :: FILTER_2:def 6
X;
coherence ;

end;

:: deftheorem defines .: FILTER_2:def 6 :

definition

let L be Lattice;
let X be Subset of (L .: );
func .: X -> Subset of L equals :: FILTER_2:def 7
X;
coherence ;

end;

:: deftheorem defines .: FILTER_2:def 7 :

registration

let L be Lattice;
let D be non empty Subset of L;
cluster D .: -> non empty ;
coherence ;

end;

registration

let L be Lattice;
let D be non empty Subset of (L .: );
cluster .: D -> non empty ;
coherence ;

end;

definition

let L be Lattice;
let S be ClosedSubset of L;
:: original: .:
redefine func S .: -> ClosedSubset of L .: ;
coherence

proof end;

end;

definition

let L be Lattice;
let S be non empty ClosedSubset of L;
:: original: .:
redefine func S .: -> non empty ClosedSubset of L .: ;
coherence

proof end;

end;

definition

let L be Lattice;
let S be ClosedSubset of L .: ;
:: original: .:
redefine func .: S -> ClosedSubset of L;
coherence

proof end;

end;

definition

let L be Lattice;
let S be non empty ClosedSubset of L .: ;
:: original: .:
redefine func .: S -> non empty ClosedSubset of L;
coherence

proof end;

end;

definition

let L be Lattice;
let F be Filter of L;
:: original: .:
redefine func F .: -> Ideal of L .: ;
coherence

proof end;

end;

definition

let L be Lattice;
let F be Filter of L .: ;
:: original: .:
redefine func .: F -> Ideal of L;
coherence

proof end;

end;

definition

let L be Lattice;
let I be Ideal of L;
:: original: .:
redefine func I .: -> Filter of L .: ;
coherence

proof end;

end;

definition

let L be Lattice;
let I be Ideal of L .: ;
:: original: .:
redefine func .: I -> Filter of L;
coherence

proof end;

end;

theorem Th22: :: FILTER_2:22

for L being Lattice
for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )

proof end;

theorem Th23: :: FILTER_2:23

for L being Lattice
for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )

proof end;

theorem :: FILTER_2:24

for L being Lattice
for I being Ideal of L ex p being Element of L st p in I

proof end;

theorem :: FILTER_2:25

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
Bottom L in I

proof end;

theorem :: FILTER_2:26

for L being Lattice st L is lower-bounded holds
{(Bottom L)} is Ideal of L

proof end;

theorem :: FILTER_2:27

for L being Lattice
for p being Element of L st {p} is Ideal of L holds
L is lower-bounded

proof end;

theorem Th28: :: FILTER_2:28

for L being Lattice holds the carrier of L is Ideal of L

proof end;

definition

let L be Lattice;
func (.L.> -> Ideal of L equals :: FILTER_2:def 8
the carrier of L;
coherence by Th28;

end;

:: deftheorem defines (. FILTER_2:def 8 :

definition

let L be Lattice;
let p be Element of L;
func (.p.> -> Ideal of L equals :: FILTER_2:def 9
{ q where q is Element of L : q [= p } ;
coherence

proof end;

end;

:: deftheorem defines (. FILTER_2:def 9 :

theorem Th29: :: FILTER_2:29

for L being Lattice
for q, p being Element of L holds
( q in (.p.> iff q [= p )

proof end;

theorem Th30: :: FILTER_2:30

for L being Lattice
for p being Element of L holds
( (.p.> = <.(p .: ).) & (.(p .: ).> = <.p.) )

proof end;

theorem :: FILTER_2:31

for L being Lattice
for p, q being Element of L holds
( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> )

proof end;

theorem :: FILTER_2:32

for L being Lattice st L is upper-bounded holds
(.L.> = (.(Top L).>

proof end;

definition

let L be Lattice;
let I be Ideal of L;
pred I is_max-ideal means :: FILTER_2:def 10
( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) );

end;

:: deftheorem defines is_max-ideal FILTER_2:def 10 :

theorem Th33: :: FILTER_2:33

for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff I .: is_ultrafilter )

proof end;

theorem :: FILTER_2:34

for L being Lattice st L is upper-bounded holds
for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is_max-ideal )

proof end;

theorem :: FILTER_2:35

for L being Lattice
for p being Element of L st ex r being Element of L st p "\/" r <> p holds
(.p.> <> the carrier of L

proof end;

theorem :: FILTER_2:36

for L being Lattice
for p being Element of L st L is upper-bounded & p <> Top L holds
ex I being Ideal of L st
( p in I & I is_max-ideal )

proof end;

definition

let L be Lattice;
let D be non empty Subset of L;
func (.D.> -> Ideal of L means :Def11: :: FILTER_2:def 11
( D c= it & ( for I being Ideal of L st D c= I holds
it c= I ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines (. FILTER_2:def 11 :

Lm1: for L1, L2 being Lattice
for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )

proof end;

theorem Th37: :: FILTER_2:37

for L being Lattice
for D being non empty Subset of L
for D' being non empty Subset of (L .: ) holds
( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D').) = (.D'.> & <.D'.) = (.(.: D').> )

proof end;

theorem Th38: :: FILTER_2:38

for L being Lattice
for I being Ideal of L holds (.I.> = I

proof end;

theorem :: FILTER_2:39

for L being Lattice
for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )

proof end;

theorem :: FILTER_2:40

for L being Lattice
for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>

proof end;

theorem :: FILTER_2:41

for L being Lattice
for p being Element of L
for D being non empty Subset of L st D = {p} holds
(.D.> = (.p.>

proof end;

theorem Th42: :: FILTER_2:42

for L being Lattice
for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )

proof end;

theorem :: FILTER_2:43

for L being Lattice
for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )

proof end;

definition

let L be Lattice;
let I be Ideal of L;
attr I is prime means :: FILTER_2:def 12
for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) );

end;

:: deftheorem defines prime FILTER_2:def 12 :

theorem Th44: :: FILTER_2:44

for L being Lattice
for I being Ideal of L holds
( I is prime iff I .: is prime )

proof end;

definition

let L be Lattice;
let D1, D2 be non empty Subset of L;
func D1 "\/" D2 -> Subset of L equals :: FILTER_2:def 13
{ (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
coherence

proof end;

end;

:: deftheorem defines "\/" FILTER_2:def 13 :

registration

let L be Lattice;
let D1, D2 be non empty Subset of L;
cluster D1 "\/" D2 -> non empty ;
coherence

proof end;

end;

Lm2: for L1, L2 being Lattice
for D1, E1 being non empty Subset of L1
for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2

proof end;

theorem Th45: :: FILTER_2:45

for L being Lattice
for D1, D2 being non empty Subset of L
for D1', D2' being non empty Subset of (L .: ) holds
( D1 "\/" D2 = (D1 .: ) "/\" (D2 .: ) & (D1 .: ) "\/" (D2 .: ) = D1 "/\" D2 & D1' "\/" D2' = (.: D1') "/\" (.: D2') & (.: D1') "\/" (.: D2') = D1' "/\" D2' )

proof end;

theorem :: FILTER_2:46

for L being Lattice
for p, q being Element of L
for D1, D2 being non empty Subset of L st p in D1 & q in D2 holds
( p "\/" q in D1 "\/" D2 & q "\/" p in D1 "\/" D2 ) ;

theorem :: FILTER_2:47

for L being Lattice
for x being set
for D1, D2 being non empty Subset of L st x in D1 "\/" D2 holds
ex p, q being Element of L st
( x = p "\/" q & p in D1 & q in D2 ) ;

theorem :: FILTER_2:48

for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1

proof end;

definition

let L be D_Lattice;
let I1, I2 be Ideal of L;
:: original: "\/"
redefine func I1 "\/" I2 -> Ideal of L;
coherence

proof end;

end;

theorem :: FILTER_2:49

for L being Lattice
for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )

proof end;

theorem :: FILTER_2:50

for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }

proof end;

theorem :: FILTER_2:51

for L being Lattice
for I, J being Ideal of L holds
( I c= I "\/" J & J c= I "\/" J )

proof end;

theorem :: FILTER_2:52

for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>

proof end;

theorem Th53: :: FILTER_2:53

for L being Lattice holds
( L is C_Lattice iff L .: is C_Lattice )

proof end;

theorem Th54: :: FILTER_2:54

for L being Lattice holds
( L is B_Lattice iff L .: is B_Lattice )

proof end;

registration

let B be B_Lattice;
cluster B .: -> Lattice-like Boolean ;
coherence by Th54;

end;

Lm3: for B being B_Lattice
for a being Element of B holds (a .: ) ` = a `

proof end;

theorem Th55: :: FILTER_2:55

for B being B_Lattice
for a being Element of B
for a' being Element of (B .: ) holds
( (a .: ) ` = a ` & (.: a') ` = a' ` )

proof end;

theorem :: FILTER_2:56

for B being B_Lattice
for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB

proof end;

theorem :: FILTER_2:57

for B being B_Lattice
for IB being Ideal of B holds
( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )

proof end;

theorem :: FILTER_2:58

for B being B_Lattice
for IB being Ideal of B holds
( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )

proof end;

theorem :: FILTER_2:59

for B being B_Lattice
for IB being Ideal of B st IB is_max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )

proof end;

theorem :: FILTER_2:60

for B being B_Lattice
for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )

proof end;

theorem Th61: :: FILTER_2:61

for L being Lattice
for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )

proof end;

theorem Th62: :: FILTER_2:62

for L being Lattice
for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 )

proof end;

definition

let L be Lattice;
let p, q be Element of L;
assume A1: p [= q ;
func [#p,q#] -> non empty ClosedSubset of L equals :Def14: :: FILTER_2:def 14
{ r where r is Element of L : ( p [= r & r [= q ) } ;
coherence

proof end;

end;

:: deftheorem Def14 defines [# FILTER_2:def 14 :

theorem Th63: :: FILTER_2:63

for L being Lattice
for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )

proof end;

theorem :: FILTER_2:64

for L being Lattice
for p, q being Element of L st p [= q holds
( p in [#p,q#] & q in [#p,q#] ) by Th63;

theorem :: FILTER_2:65

for L being Lattice
for p being Element of L holds [#p,p#] = {p}

proof end;

theorem :: FILTER_2:66

for L being Lattice
for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]

proof end;

theorem :: FILTER_2:67

for L being Lattice
for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]

proof end;

theorem :: FILTER_2:68

for L1, L2 being Lattice
for F1 being Filter of L1
for F2 being Filter of L2 st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2

proof end;

notation

let L be Lattice;
synonym Sublattice of L for SubLattice of L;

end;

definition

let L be Lattice;
redefine mode SubLattice of L means :Def15: :: FILTER_2:def 15
ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of it,the L_join of it,the L_meet of it #) = LattStr(# P,o1,o2 #) );
compatibility

proof end;

end;

:: deftheorem Def15 defines Sublattice FILTER_2:def 15 :

theorem Th69: :: FILTER_2:69

for L being Lattice
for K being Sublattice of L
for a being Element of K holds a is Element of L

proof end;

definition

let L be Lattice;
let P be non empty ClosedSubset of L;
func latt L,P -> Sublattice of L means :Def16: :: FILTER_2:def 16
ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & it = LattStr(# P,o1,o2 #) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def16 defines latt FILTER_2:def 16 :

registration

let L be Lattice;
let P be non empty ClosedSubset of L;
cluster latt L,P -> strict ;
coherence

proof end;

end;

definition

let L be Lattice;
let l be Sublattice of L;
:: original: .:
redefine func l .: -> strict Sublattice of L .: ;
coherence

proof end;

end;

theorem Th70: :: FILTER_2:70

for L being Lattice
for F being Filter of L holds latt F = latt L,F

proof end;

theorem Th71: :: FILTER_2:71

for L being Lattice
for P being non empty ClosedSubset of L holds latt L,P = (latt (L .: ),(P .: )) .:

proof end;

theorem :: FILTER_2:72

for L being Lattice holds
( latt L,(.L.> = LattStr(# the carrier of L,the L_join of L,the L_meet of L #) & latt L,<.L.) = LattStr(# the carrier of L,the L_join of L,the L_meet of L #) )

proof end;

theorem Th73: :: FILTER_2:73

for L being Lattice
for P being non empty ClosedSubset of L holds
( the carrier of (latt L,P) = P & the L_join of (latt L,P) = the L_join of L || P & the L_meet of (latt L,P) = the L_meet of L || P )

proof end;

theorem Th74: :: FILTER_2:74

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p', q' being Element of (latt L,P) st p = p' & q = q' holds
( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )

proof end;

theorem Th75: :: FILTER_2:75

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p', q' being Element of (latt L,P) st p = p' & q = q' holds
( p [= q iff p' [= q' )

proof end;

theorem :: FILTER_2:76

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
latt L,I is lower-bounded

proof end;

theorem :: FILTER_2:77

for L being Lattice
for P being non empty ClosedSubset of L st L is modular holds
latt L,P is modular

proof end;

theorem Th78: :: FILTER_2:78

for L being Lattice
for P being non empty ClosedSubset of L st L is distributive holds
latt L,P is distributive

proof end;

theorem :: FILTER_2:79

for L being Lattice
for p, q being Element of L st L is implicative & p [= q holds
latt L,[#p,q#] is implicative

proof end;

theorem Th80: :: FILTER_2:80

for L being Lattice
for p being Element of L holds latt L,(.p.> is upper-bounded

proof end;

theorem Th81: :: FILTER_2:81

for L being Lattice
for p being Element of L holds Top (latt L,(.p.>) = p

proof end;

theorem Th82: :: FILTER_2:82

for L being Lattice
for p being Element of L st L is lower-bounded holds
( latt L,(.p.> is lower-bounded & Bottom (latt L,(.p.>) = Bottom L )

proof end;

theorem Th83: :: FILTER_2:83

for L being Lattice
for p being Element of L st L is lower-bounded holds
latt L,(.p.> is bounded

proof end;

theorem Th84: :: FILTER_2:84

for L being Lattice
for p, q being Element of L st p [= q holds
( latt L,[#p,q#] is bounded & Top (latt L,[#p,q#]) = q & Bottom (latt L,[#p,q#]) = p )

proof end;

theorem :: FILTER_2:85

for L being Lattice
for p being Element of L st L is C_Lattice & L is modular holds
latt L,(.p.> is C_Lattice

proof end;

theorem Th86: :: FILTER_2:86

for L being Lattice
for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt L,[#p,q#] is C_Lattice

proof end;

theorem :: FILTER_2:87

for L being Lattice
for p, q being Element of L st L is B_Lattice & p [= q holds
latt L,[#p,q#] is B_Lattice

proof end;