:: LATTICE4 semantic presentation begin theorem :: LATTICE4:1 for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) holds ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) proof let X be set ; ::_thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) implies ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) ) assume that A1: X <> {} and A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ; ::_thesis: ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) for Z being set st Z c= X & Z is c=-linear holds ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) proof let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) assume A3: ( Z c= X & Z is c=-linear ) ; ::_thesis: ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) percases ( Z = {} or Z <> {} ) ; supposeA4: Z = {} ; ::_thesis: ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) set Y = the Element of X; for X1 being set st X1 in Z holds X1 c= the Element of X by A4; hence ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) by A1; ::_thesis: verum end; suppose Z <> {} ; ::_thesis: ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) hence ex Y being set st ( Y in X & ( for X1 being set st X1 in Z holds X1 c= Y ) ) by A2, A3; ::_thesis: verum end; end; end; hence ex Y being set st ( Y in X & ( for Z being set st Z in X & Z <> Y holds not Y c= Z ) ) by A1, ORDERS_1:65; ::_thesis: verum end; begin registration let L be Lattice; cluster<.L.) -> prime ; coherence <.L.) is prime proof let p be Element of L; :: according to FILTER_0:def_5 ::_thesis: for b1 being Element of the carrier of L holds ( ( not p "\/" b1 in <.L.) or p in <.L.) or b1 in <.L.) ) & ( ( not p in <.L.) & not b1 in <.L.) ) or p "\/" b1 in <.L.) ) ) thus for b1 being Element of the carrier of L holds ( ( not p "\/" b1 in <.L.) or p in <.L.) or b1 in <.L.) ) & ( ( not p in <.L.) & not b1 in <.L.) ) or p "\/" b1 in <.L.) ) ) ; ::_thesis: verum end; end; theorem :: LATTICE4:2 for L being Lattice for F, H being Filter of L holds ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) proof let L be Lattice; ::_thesis: for F, H being Filter of L holds ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) let F, H be Filter of L; ::_thesis: ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) A1: F \/ H c= <.(F \/ H).) by FILTER_0:def_4; ( F c= F \/ H & H c= F \/ H ) by XBOOLE_1:7; hence ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: LATTICE4:3 for L being Lattice for F being Filter of L for p, q being Element of L st p in <.(<.q.) \/ F).) holds ex r being Element of L st ( r in F & q "/\" r [= p ) proof let L be Lattice; ::_thesis: for F being Filter of L for p, q being Element of L st p in <.(<.q.) \/ F).) holds ex r being Element of L st ( r in F & q "/\" r [= p ) let F be Filter of L; ::_thesis: for p, q being Element of L st p in <.(<.q.) \/ F).) holds ex r being Element of L st ( r in F & q "/\" r [= p ) let p, q be Element of L; ::_thesis: ( p in <.(<.q.) \/ F).) implies ex r being Element of L st ( r in F & q "/\" r [= p ) ) A1: <.(<.q.) \/ F).) = { r where r is Element of L : ex p9, q9 being Element of L st ( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) } by FILTER_0:35; assume p in <.(<.q.) \/ F).) ; ::_thesis: ex r being Element of L st ( r in F & q "/\" r [= p ) then ex r being Element of L st ( r = p & ex p9, q9 being Element of L st ( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) ) by A1; then consider p9, q9 being Element of L such that A2: p9 "/\" q9 [= p and A3: p9 in <.q.) and A4: q9 in F ; q [= p9 by A3, FILTER_0:15; then q "/\" q9 [= p9 "/\" q9 by LATTICES:9; hence ex r being Element of L st ( r in F & q "/\" r [= p ) by A2, A4, LATTICES:7; ::_thesis: verum end; definition let L1, L2 be Lattice; mode Homomorphism of L1,L2 -> Function of the carrier of L1, the carrier of L2 means :Def1: :: LATTICE4:def 1 for a1, b1 being Element of L1 holds ( it . (a1 "\/" b1) = (it . a1) "\/" (it . b1) & it . (a1 "/\" b1) = (it . a1) "/\" (it . b1) ); existence ex b1 being Function of the carrier of L1, the carrier of L2 st for a1, b1 being Element of L1 holds ( b1 . (a1 "\/" b1) = (b1 . a1) "\/" (b1 . b1) & b1 . (a1 "/\" b1) = (b1 . a1) "/\" (b1 . b1) ) proof set b = the Element of L2; defpred S1[ set , set ] means for a1 being Element of L1 st \$1 = a1 holds \$2 = the Element of L2; A1: now__::_thesis:_for_x_being_Element_of_L1_ex_b_being_Element_of_L2_st_S1[x,b] let x be Element of L1; ::_thesis: ex b being Element of L2 st S1[x,b] take b = the Element of L2; ::_thesis: S1[x,b] thus S1[x,b] ; ::_thesis: verum end; consider f being Function of the carrier of L1, the carrier of L2 such that A2: for x being Element of L1 holds S1[x,f . x] from FUNCT_2:sch_3(A1); take f ; ::_thesis: for a1, b1 being Element of L1 holds ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) now__::_thesis:_for_a1,_b1_being_Element_of_L1_holds_ (_f_._(a1_"\/"_b1)_=_(f_._a1)_"\/"_(f_._b1)_&_f_._(a1_"/\"_b1)_=_(f_._a1)_"/\"_(f_._b1)_) let a1, b1 be Element of L1; ::_thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) thus f . (a1 "\/" b1) = the Element of L2 by A2 .= the Element of L2 "\/" the Element of L2 .= (f . a1) "\/" the Element of L2 by A2 .= (f . a1) "\/" (f . b1) by A2 ; ::_thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) thus f . (a1 "/\" b1) = the Element of L2 by A2 .= the Element of L2 "/\" the Element of L2 .= (f . a1) "/\" the Element of L2 by A2 .= (f . a1) "/\" (f . b1) by A2 ; ::_thesis: verum end; hence for a1, b1 being Element of L1 holds ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines Homomorphism LATTICE4:def_1_:_ for L1, L2 being Lattice for b3 being Function of the carrier of L1, the carrier of L2 holds ( b3 is Homomorphism of L1,L2 iff for a1, b1 being Element of L1 holds ( b3 . (a1 "\/" b1) = (b3 . a1) "\/" (b3 . b1) & b3 . (a1 "/\" b1) = (b3 . a1) "/\" (b3 . b1) ) ); theorem Th4: :: LATTICE4:4 for L1, L2 being Lattice for a1, b1 being Element of L1 for f being Homomorphism of L1,L2 st a1 [= b1 holds f . a1 [= f . b1 proof let L1, L2 be Lattice; ::_thesis: for a1, b1 being Element of L1 for f being Homomorphism of L1,L2 st a1 [= b1 holds f . a1 [= f . b1 let a1, b1 be Element of L1; ::_thesis: for f being Homomorphism of L1,L2 st a1 [= b1 holds f . a1 [= f . b1 let f be Homomorphism of L1,L2; ::_thesis: ( a1 [= b1 implies f . a1 [= f . b1 ) assume A1: a1 [= b1 ; ::_thesis: f . a1 [= f . b1 (f . a1) "\/" (f . b1) = f . (a1 "\/" b1) by Def1 .= f . b1 by A1, LATTICES:def_3 ; hence f . a1 [= f . b1 by LATTICES:def_3; ::_thesis: verum end; theorem Th5: :: LATTICE4:5 for L1, L2 being Lattice for a1, b1 being Element of L1 for f being Homomorphism of L1,L2 st f is one-to-one holds ( a1 [= b1 iff f . a1 [= f . b1 ) proof let L1, L2 be Lattice; ::_thesis: for a1, b1 being Element of L1 for f being Homomorphism of L1,L2 st f is one-to-one holds ( a1 [= b1 iff f . a1 [= f . b1 ) let a1, b1 be Element of L1; ::_thesis: for f being Homomorphism of L1,L2 st f is one-to-one holds ( a1 [= b1 iff f . a1 [= f . b1 ) let f be Homomorphism of L1,L2; ::_thesis: ( f is one-to-one implies ( a1 [= b1 iff f . a1 [= f . b1 ) ) assume A1: f is one-to-one ; ::_thesis: ( a1 [= b1 iff f . a1 [= f . b1 ) reconsider f = f as Function of the carrier of L1, the carrier of L2 ; ( f . a1 [= f . b1 implies a1 [= b1 ) proof assume f . a1 [= f . b1 ; ::_thesis: a1 [= b1 then (f . a1) "\/" (f . b1) = f . b1 by LATTICES:def_3; then f . (a1 "\/" b1) = f . b1 by Def1; hence a1 "\/" b1 = b1 by A1, FUNCT_2:19; :: according to LATTICES:def_3 ::_thesis: verum end; hence ( a1 [= b1 iff f . a1 [= f . b1 ) by Th4; ::_thesis: verum end; theorem Th6: :: LATTICE4:6 for L1, L2 being Lattice for f being Function of the carrier of L1, the carrier of L2 st f is onto holds for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 proof let L1, L2 be Lattice; ::_thesis: for f being Function of the carrier of L1, the carrier of L2 st f is onto holds for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( f is onto implies for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 ) reconsider g = f as Function of the carrier of L1, the carrier of L2 ; assume f is onto ; ::_thesis: for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 then A1: rng g = the carrier of L2 by FUNCT_2:def_3; now__::_thesis:_for_a2_being_Element_of_L2_ex_a1_being_Element_of_L1_st_g_._a1_=_a2 let a2 be Element of L2; ::_thesis: ex a1 being Element of L1 st g . a1 = a2 ex x being set st ( x in the carrier of L1 & g . x = a2 ) by A1, FUNCT_2:11; hence ex a1 being Element of L1 st g . a1 = a2 ; ::_thesis: verum end; hence for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 ; ::_thesis: verum end; definition let L1, L2 be Lattice; redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 2 ex f being Homomorphism of L1,L2 st f is bijective ; compatibility ( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective ) proof thus ( L1,L2 are_isomorphic implies ex f being Homomorphism of L1,L2 st f is bijective ) ::_thesis: ( ex f being Homomorphism of L1,L2 st f is bijective implies L1,L2 are_isomorphic ) proof set R = LattRel L1; set S = LattRel L2; assume L1,L2 are_isomorphic ; ::_thesis: ex f being Homomorphism of L1,L2 st f is bijective then LattRel L1, LattRel L2 are_isomorphic by FILTER_1:def_9; then consider F being Function such that A1: F is_isomorphism_of LattRel L1, LattRel L2 by WELLORD1:def_8; A2: dom F = field (LattRel L1) by A1, WELLORD1:def_7; A3: ( field (LattRel L2) = the carrier of L2 & rng F = field (LattRel L2) ) by A1, FILTER_1:32, WELLORD1:def_7; A4: field (LattRel L1) = the carrier of L1 by FILTER_1:32; then reconsider F = F as Function of the carrier of L1, the carrier of L2 by A2, A3, FUNCT_2:1; now__::_thesis:_for_a1,_b1_being_Element_of_L1_holds_ (_F_._(a1_"\/"_b1)_=_(F_._a1)_"\/"_(F_._b1)_&_F_._(a1_"/\"_b1)_=_(F_._a1)_"/\"_(F_._b1)_) let a1, b1 be Element of L1; ::_thesis: ( F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) & F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) ) reconsider a19 = a1, b19 = b1 as Element of L1 ; A5: F is onto by A3, FUNCT_2:def_3; thus F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) ::_thesis: F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) proof b19 [= a19 "\/" b19 by LATTICES:5; then [b1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31; then [(F . b1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def_7; then A6: F . b19 [= F . (a19 "\/" b19) by FILTER_1:31; consider k1 being Element of L1 such that A7: (F . a1) "\/" (F . b1) = F . k1 by A5, Th6; F . b1 [= F . k1 by A7, LATTICES:5; then [(F . b1),(F . k1)] in LattRel L2 by FILTER_1:31; then [b1,k1] in LattRel L1 by A1, A4, WELLORD1:def_7; then A8: b1 [= k1 by FILTER_1:31; F . a1 [= F . k1 by A7, LATTICES:5; then [(F . a1),(F . k1)] in LattRel L2 by FILTER_1:31; then [a1,k1] in LattRel L1 by A1, A4, WELLORD1:def_7; then a1 [= k1 by FILTER_1:31; then a1 "\/" b1 [= k1 by A8, FILTER_0:6; then [(a1 "\/" b1),k1] in LattRel L1 by FILTER_1:31; then [(F . (a1 "\/" b1)),(F . k1)] in LattRel L2 by A1, WELLORD1:def_7; then A9: F . (a1 "\/" b1) [= (F . a1) "\/" (F . b1) by A7, FILTER_1:31; a19 [= a19 "\/" b19 by LATTICES:5; then [a1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31; then [(F . a1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def_7; then F . a19 [= F . (a19 "\/" b19) by FILTER_1:31; then (F . a1) "\/" (F . b1) [= F . (a1 "\/" b1) by A6, FILTER_0:6; hence F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) by A9, LATTICES:8; ::_thesis: verum end; thus F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) ::_thesis: verum proof a19 "/\" b19 [= b19 by LATTICES:6; then [(a1 "/\" b1),b1] in LattRel L1 by FILTER_1:31; then [(F . (a1 "/\" b1)),(F . b1)] in LattRel L2 by A1, WELLORD1:def_7; then A10: F . (a19 "/\" b19) [= F . b19 by FILTER_1:31; consider k1 being Element of L1 such that A11: (F . a1) "/\" (F . b1) = F . k1 by A5, Th6; F . k1 [= F . b1 by A11, LATTICES:6; then [(F . k1),(F . b1)] in LattRel L2 by FILTER_1:31; then [k1,b1] in LattRel L1 by A1, A4, WELLORD1:def_7; then A12: k1 [= b1 by FILTER_1:31; F . k1 [= F . a1 by A11, LATTICES:6; then [(F . k1),(F . a1)] in LattRel L2 by FILTER_1:31; then [k1,a1] in LattRel L1 by A1, A4, WELLORD1:def_7; then k1 [= a1 by FILTER_1:31; then k1 [= a1 "/\" b1 by A12, FILTER_0:7; then [k1,(a1 "/\" b1)] in LattRel L1 by FILTER_1:31; then [(F . k1),(F . (a1 "/\" b1))] in LattRel L2 by A1, WELLORD1:def_7; then A13: (F . a1) "/\" (F . b1) [= F . (a1 "/\" b1) by A11, FILTER_1:31; a19 "/\" b19 [= a19 by LATTICES:6; then [(a1 "/\" b1),a1] in LattRel L1 by FILTER_1:31; then [(F . (a1 "/\" b1)),(F . a1)] in LattRel L2 by A1, WELLORD1:def_7; then F . (a19 "/\" b19) [= F . a19 by FILTER_1:31; then F . (a1 "/\" b1) [= (F . a1) "/\" (F . b1) by A10, FILTER_0:7; hence F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) by A13, LATTICES:8; ::_thesis: verum end; end; then reconsider F = F as Homomorphism of L1,L2 by Def1; take F ; ::_thesis: F is bijective ( F is one-to-one & F is onto ) by A1, A3, FUNCT_2:def_3, WELLORD1:def_7; hence F is bijective ; ::_thesis: verum end; set R = LattRel L1; set S = LattRel L2; given f being Homomorphism of L1,L2 such that A14: f is bijective ; ::_thesis: L1,L2 are_isomorphic A15: for a, b being set holds ( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) ) proof let a, b be set ; ::_thesis: ( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) ) hereby ::_thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 implies [a,b] in LattRel L1 ) assume A16: [a,b] in LattRel L1 ; ::_thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) hence ( a in field (LattRel L1) & b in field (LattRel L1) ) by RELAT_1:15; ::_thesis: [(f . a),(f . b)] in LattRel L2 then reconsider a9 = a, b9 = b as Element of L1 by FILTER_1:32; a9 [= b9 by A16, FILTER_1:31; then f . a9 [= f . b9 by A14, Th5; hence [(f . a),(f . b)] in LattRel L2 by FILTER_1:31; ::_thesis: verum end; assume that A17: ( a in field (LattRel L1) & b in field (LattRel L1) ) and A18: [(f . a),(f . b)] in LattRel L2 ; ::_thesis: [a,b] in LattRel L1 reconsider a9 = a, b9 = b as Element of L1 by A17, FILTER_1:32; f . a9 [= f . b9 by A18, FILTER_1:31; then a9 [= b9 by A14, Th5; hence [a,b] in LattRel L1 by FILTER_1:31; ::_thesis: verum end; A19: dom f = the carrier of L1 by FUNCT_2:def_1 .= field (LattRel L1) by FILTER_1:32 ; rng f = the carrier of L2 by A14, FUNCT_2:def_3 .= field (LattRel L2) by FILTER_1:32 ; then f is_isomorphism_of LattRel L1, LattRel L2 by A14, A19, A15, WELLORD1:def_7; then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def_8; hence L1,L2 are_isomorphic by FILTER_1:def_9; ::_thesis: verum end; end; :: deftheorem defines are_isomorphic LATTICE4:def_2_:_ for L1, L2 being Lattice holds ( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective ); definition let L1, L2 be Lattice; let f be Homomorphism of L1,L2; predf preserves_implication means :Def3: :: LATTICE4:def 3 for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1); predf preserves_top means :Def4: :: LATTICE4:def 4 f . (Top L1) = Top L2; predf preserves_bottom means :Def5: :: LATTICE4:def 5 f . (Bottom L1) = Bottom L2; predf preserves_complement means :Def6: :: LATTICE4:def 6 for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ; end; :: deftheorem Def3 defines preserves_implication LATTICE4:def_3_:_ for L1, L2 being Lattice for f being Homomorphism of L1,L2 holds ( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) ); :: deftheorem Def4 defines preserves_top LATTICE4:def_4_:_ for L1, L2 being Lattice for f being Homomorphism of L1,L2 holds ( f preserves_top iff f . (Top L1) = Top L2 ); :: deftheorem Def5 defines preserves_bottom LATTICE4:def_5_:_ for L1, L2 being Lattice for f being Homomorphism of L1,L2 holds ( f preserves_bottom iff f . (Bottom L1) = Bottom L2 ); :: deftheorem Def6 defines preserves_complement LATTICE4:def_6_:_ for L1, L2 being Lattice for f being Homomorphism of L1,L2 holds ( f preserves_complement iff for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ); definition let L be Lattice; mode ClosedSubset of L is meet-closed join-closed Subset of L; end; theorem Th7: :: LATTICE4:7 for L being Lattice holds the carrier of L is ClosedSubset of L proof let L be Lattice; ::_thesis: the carrier of L is ClosedSubset of L the carrier of L c= the carrier of L ; then reconsider F = the carrier of L as Subset of L ; A1: for p, q being Element of L st p in F & q in F holds p "/\" q in F ; for p, q being Element of L st p in F & q in F holds p "\/" q in F ; hence the carrier of L is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum end; registration let L be Lattice; cluster non empty meet-closed join-closed for Element of bool the carrier of L; existence not for b1 being ClosedSubset of L holds b1 is empty proof the carrier of L is ClosedSubset of L by Th7; hence not for b1 being ClosedSubset of L holds b1 is empty ; ::_thesis: verum end; end; theorem :: LATTICE4:8 for L being Lattice for F being Filter of L holds F is ClosedSubset of L ; definition let L be Lattice; let B be Finite_Subset of the carrier of L; func FinJoin B -> Element of L equals :: LATTICE4:def 7 FinJoin (B,(id L)); coherence FinJoin (B,(id L)) is Element of L ; func FinMeet B -> Element of L equals :: LATTICE4:def 8 FinMeet (B,(id L)); coherence FinMeet (B,(id L)) is Element of L ; end; :: deftheorem defines FinJoin LATTICE4:def_7_:_ for L being Lattice for B being Finite_Subset of the carrier of L holds FinJoin B = FinJoin (B,(id L)); :: deftheorem defines FinMeet LATTICE4:def_8_:_ for L being Lattice for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet (B,(id L)); theorem Th9: :: LATTICE4:9 for L being Lattice for p being Element of L holds FinJoin {.p.} = p proof let L be Lattice; ::_thesis: for p being Element of L holds FinJoin {.p.} = p let p be Element of L; ::_thesis: FinJoin {.p.} = p thus FinJoin {.p.} = the L_join of L \$\$ ({.p.},(id L)) by LATTICE2:def_3 .= (id L) . p by SETWISEO:17 .= p by FUNCT_1:18 ; ::_thesis: verum end; theorem Th10: :: LATTICE4:10 for L being Lattice for p being Element of L holds FinMeet {.p.} = p proof let L be Lattice; ::_thesis: for p being Element of L holds FinMeet {.p.} = p let p be Element of L; ::_thesis: FinMeet {.p.} = p set M = the L_meet of L; thus FinMeet {.p.} = the L_meet of L \$\$ ({.p.},(id L)) by LATTICE2:def_4 .= (id L) . p by SETWISEO:17 .= p by FUNCT_1:18 ; ::_thesis: verum end; begin theorem Th11: :: LATTICE4:11 for L2 being Lattice for DL being distributive Lattice for f being Homomorphism of DL,L2 st f is onto holds L2 is distributive proof let L2 be Lattice; ::_thesis: for DL being distributive Lattice for f being Homomorphism of DL,L2 st f is onto holds L2 is distributive let DL be distributive Lattice; ::_thesis: for f being Homomorphism of DL,L2 st f is onto holds L2 is distributive let f be Homomorphism of DL,L2; ::_thesis: ( f is onto implies L2 is distributive ) assume A1: f is onto ; ::_thesis: L2 is distributive thus L2 is distributive ::_thesis: verum proof let a, b, c be Element of L2; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) consider a9 being Element of DL such that A2: f . a9 = a by A1, Th6; consider c9 being Element of DL such that A3: f . c9 = c by A1, Th6; consider b9 being Element of DL such that A4: f . b9 = b by A1, Th6; thus a "/\" (b "\/" c) = a "/\" (f . (b9 "\/" c9)) by A4, A3, Def1 .= f . (a9 "/\" (b9 "\/" c9)) by A2, Def1 .= f . ((a9 "/\" b9) "\/" (a9 "/\" c9)) by LATTICES:def_11 .= (f . (a9 "/\" b9)) "\/" (f . (a9 "/\" c9)) by Def1 .= (a "/\" b) "\/" (f . (a9 "/\" c9)) by A2, A4, Def1 .= (a "/\" b) "\/" (a "/\" c) by A2, A3, Def1 ; ::_thesis: verum end; end; begin theorem Th12: :: LATTICE4:12 for L2 being Lattice for 0L being lower-bounded Lattice for f being Homomorphism of 0L,L2 st f is onto holds ( L2 is lower-bounded & f preserves_bottom ) proof let L2 be Lattice; ::_thesis: for 0L being lower-bounded Lattice for f being Homomorphism of 0L,L2 st f is onto holds ( L2 is lower-bounded & f preserves_bottom ) let 0L be lower-bounded Lattice; ::_thesis: for f being Homomorphism of 0L,L2 st f is onto holds ( L2 is lower-bounded & f preserves_bottom ) let f be Homomorphism of 0L,L2; ::_thesis: ( f is onto implies ( L2 is lower-bounded & f preserves_bottom ) ) set r = f . (Bottom 0L); assume A1: f is onto ; ::_thesis: ( L2 is lower-bounded & f preserves_bottom ) A2: now__::_thesis:_for_a2_being_Element_of_L2_holds_ (_(f_._(Bottom_0L))_"/\"_a2_=_f_._(Bottom_0L)_&_a2_"/\"_(f_._(Bottom_0L))_=_f_._(Bottom_0L)_) let a2 be Element of L2; ::_thesis: ( (f . (Bottom 0L)) "/\" a2 = f . (Bottom 0L) & a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ) consider a1 being Element of 0L such that A3: f . a1 = a2 by A1, Th6; thus (f . (Bottom 0L)) "/\" a2 = f . ((Bottom 0L) "/\" a1) by A3, Def1 .= f . (Bottom 0L) by LATTICES:15 ; ::_thesis: a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) hence a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ; ::_thesis: verum end; thus L2 is lower-bounded ::_thesis: f preserves_bottom proof take f . (Bottom 0L) ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L2 holds ( (f . (Bottom 0L)) "/\" b1 = f . (Bottom 0L) & b1 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ) thus for b1 being Element of the carrier of L2 holds ( (f . (Bottom 0L)) "/\" b1 = f . (Bottom 0L) & b1 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ) by A2; ::_thesis: verum end; then Bottom L2 = f . (Bottom 0L) by A2, LATTICES:def_16; hence f preserves_bottom by Def5; ::_thesis: verum end; theorem Th13: :: LATTICE4:13 for 0L being lower-bounded Lattice for B being Finite_Subset of the carrier of 0L for b being Element of 0L for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b) proof let 0L be lower-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 0L for b being Element of 0L for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b) let B be Finite_Subset of the carrier of 0L; ::_thesis: for b being Element of 0L for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b) let b be Element of 0L; ::_thesis: for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b) let f be UnOp of the carrier of 0L; ::_thesis: FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b) set J = the L_join of 0L; thus FinJoin ((B \/ {.b.}),f) = the L_join of 0L \$\$ ((B \/ {.b.}),f) by LATTICE2:def_3 .= ( the L_join of 0L \$\$ (B,f)) "\/" (f . b) by SETWISEO:32 .= (FinJoin (B,f)) "\/" (f . b) by LATTICE2:def_3 ; ::_thesis: verum end; theorem Th14: :: LATTICE4:14 for 0L being lower-bounded Lattice for B being Finite_Subset of the carrier of 0L for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b proof let 0L be lower-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 0L for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b let B be Finite_Subset of the carrier of 0L; ::_thesis: for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b let b be Element of 0L; ::_thesis: FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b thus FinJoin (B \/ {.b.}) = (FinJoin (B,(id 0L))) "\/" ((id 0L) . b) by Th13 .= (FinJoin B) "\/" b by FUNCT_1:18 ; ::_thesis: verum end; theorem :: LATTICE4:15 for 0L being lower-bounded Lattice for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2) proof let 0L be lower-bounded Lattice; ::_thesis: for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2) let B1, B2 be Finite_Subset of the carrier of 0L; ::_thesis: (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2) set J = the L_join of 0L; thus FinJoin (B1 \/ B2) = the L_join of 0L \$\$ ((B1 \/ B2),(id 0L)) by LATTICE2:def_3 .= ( the L_join of 0L \$\$ (B1,(id 0L))) "\/" ( the L_join of 0L \$\$ (B2,(id 0L))) by SETWISEO:33 .= (FinJoin B1) "\/" ( the L_join of 0L \$\$ (B2,(id 0L))) by LATTICE2:def_3 .= (FinJoin B1) "\/" (FinJoin B2) by LATTICE2:def_3 ; ::_thesis: verum end; Lm1: for 0L being lower-bounded Lattice for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L proof let 0L be lower-bounded Lattice; ::_thesis: for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L let f be Function of the carrier of 0L, the carrier of 0L; ::_thesis: FinJoin (({}. the carrier of 0L),f) = Bottom 0L set J = the L_join of 0L; thus FinJoin (({}. the carrier of 0L),f) = the L_join of 0L \$\$ (({}. the carrier of 0L),f) by LATTICE2:def_3 .= the_unity_wrt the L_join of 0L by SETWISEO:31 .= Bottom 0L by LATTICE2:52 ; ::_thesis: verum end; theorem :: LATTICE4:16 for 0L being lower-bounded Lattice holds FinJoin ({}. the carrier of 0L) = Bottom 0L by Lm1; theorem Th17: :: LATTICE4:17 for 0L being lower-bounded Lattice for A being ClosedSubset of 0L st Bottom 0L in A holds for B being Finite_Subset of the carrier of 0L st B c= A holds FinJoin B in A proof let 0L be lower-bounded Lattice; ::_thesis: for A being ClosedSubset of 0L st Bottom 0L in A holds for B being Finite_Subset of the carrier of 0L st B c= A holds FinJoin B in A let A be ClosedSubset of 0L; ::_thesis: ( Bottom 0L in A implies for B being Finite_Subset of the carrier of 0L st B c= A holds FinJoin B in A ) defpred S1[ Finite_Subset of the carrier of 0L] means ( \$1 c= A implies FinJoin \$1 in A ); A1: for B1 being Finite_Subset of the carrier of 0L for p being Element of 0L st S1[B1] holds S1[B1 \/ {.p.}] proof let B1 be Finite_Subset of the carrier of 0L; ::_thesis: for p being Element of 0L st S1[B1] holds S1[B1 \/ {.p.}] let p be Element of 0L; ::_thesis: ( S1[B1] implies S1[B1 \/ {.p.}] ) assume A2: ( B1 c= A implies FinJoin B1 in A ) ; ::_thesis: S1[B1 \/ {.p.}] assume A3: B1 \/ {p} c= A ; ::_thesis: FinJoin (B1 \/ {.p.}) in A then {p} c= A by XBOOLE_1:11; then p in A by ZFMISC_1:31; then (FinJoin B1) "\/" p in A by A2, A3, LATTICES:def_25, XBOOLE_1:11; hence FinJoin (B1 \/ {.p.}) in A by Th14; ::_thesis: verum end; assume Bottom 0L in A ; ::_thesis: for B being Finite_Subset of the carrier of 0L st B c= A holds FinJoin B in A then A4: S1[ {}. the carrier of 0L] by Lm1; thus for B being Element of Fin the carrier of 0L holds S1[B] from SETWISEO:sch_4(A4, A1); ::_thesis: verum end; begin theorem Th18: :: LATTICE4:18 for L2 being Lattice for 1L being upper-bounded Lattice for f being Homomorphism of 1L,L2 st f is onto holds ( L2 is upper-bounded & f preserves_top ) proof let L2 be Lattice; ::_thesis: for 1L being upper-bounded Lattice for f being Homomorphism of 1L,L2 st f is onto holds ( L2 is upper-bounded & f preserves_top ) let 1L be upper-bounded Lattice; ::_thesis: for f being Homomorphism of 1L,L2 st f is onto holds ( L2 is upper-bounded & f preserves_top ) let f be Homomorphism of 1L,L2; ::_thesis: ( f is onto implies ( L2 is upper-bounded & f preserves_top ) ) set r = f . (Top 1L); assume A1: f is onto ; ::_thesis: ( L2 is upper-bounded & f preserves_top ) A2: now__::_thesis:_for_a2_being_Element_of_L2_holds_ (_(f_._(Top_1L))_"\/"_a2_=_f_._(Top_1L)_&_a2_"\/"_(f_._(Top_1L))_=_f_._(Top_1L)_) let a2 be Element of L2; ::_thesis: ( (f . (Top 1L)) "\/" a2 = f . (Top 1L) & a2 "\/" (f . (Top 1L)) = f . (Top 1L) ) consider a1 being Element of 1L such that A3: f . a1 = a2 by A1, Th6; thus (f . (Top 1L)) "\/" a2 = f . ((Top 1L) "\/" a1) by A3, Def1 .= f . (Top 1L) by LATTICES:18 ; ::_thesis: a2 "\/" (f . (Top 1L)) = f . (Top 1L) hence a2 "\/" (f . (Top 1L)) = f . (Top 1L) ; ::_thesis: verum end; thus L2 is upper-bounded ::_thesis: f preserves_top proof take f . (Top 1L) ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L2 holds ( (f . (Top 1L)) "\/" b1 = f . (Top 1L) & b1 "\/" (f . (Top 1L)) = f . (Top 1L) ) thus for b1 being Element of the carrier of L2 holds ( (f . (Top 1L)) "\/" b1 = f . (Top 1L) & b1 "\/" (f . (Top 1L)) = f . (Top 1L) ) by A2; ::_thesis: verum end; then Top L2 = f . (Top 1L) by A2, LATTICES:def_17; hence f preserves_top by Def4; ::_thesis: verum end; Lm2: for 1L being upper-bounded Lattice for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L proof let 1L be upper-bounded Lattice; ::_thesis: for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L let f be Function of the carrier of 1L, the carrier of 1L; ::_thesis: FinMeet (({}. the carrier of 1L),f) = Top 1L set M = the L_meet of 1L; thus FinMeet (({}. the carrier of 1L),f) = the L_meet of 1L \$\$ (({}. the carrier of 1L),f) by LATTICE2:def_4 .= the_unity_wrt the L_meet of 1L by SETWISEO:31 .= Top 1L by LATTICE2:57 ; ::_thesis: verum end; theorem :: LATTICE4:19 for 1L being upper-bounded Lattice holds FinMeet ({}. the carrier of 1L) = Top 1L by Lm2; theorem Th20: :: LATTICE4:20 for 1L being upper-bounded Lattice for B being Finite_Subset of the carrier of 1L for b being Element of 1L for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b) proof let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L for b being Element of 1L for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b) let B be Finite_Subset of the carrier of 1L; ::_thesis: for b being Element of 1L for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b) let b be Element of 1L; ::_thesis: for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b) let f be UnOp of the carrier of 1L; ::_thesis: FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b) set M = the L_meet of 1L; thus FinMeet ((B \/ {.b.}),f) = the L_meet of 1L \$\$ ((B \/ {.b.}),f) by LATTICE2:def_4 .= ( the L_meet of 1L \$\$ (B,f)) "/\" (f . b) by SETWISEO:32 .= (FinMeet (B,f)) "/\" (f . b) by LATTICE2:def_4 ; ::_thesis: verum end; theorem Th21: :: LATTICE4:21 for 1L being upper-bounded Lattice for B being Finite_Subset of the carrier of 1L for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b proof let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b let B be Finite_Subset of the carrier of 1L; ::_thesis: for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b let b be Element of 1L; ::_thesis: FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b thus FinMeet (B \/ {.b.}) = (FinMeet (B,(id 1L))) "/\" ((id 1L) . b) by Th20 .= (FinMeet B) "/\" b by FUNCT_1:18 ; ::_thesis: verum end; theorem Th22: :: LATTICE4:22 for 1L being upper-bounded Lattice for B being Finite_Subset of the carrier of 1L for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f)) proof let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f)) let B be Finite_Subset of the carrier of 1L; ::_thesis: for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f)) let f, g be UnOp of the carrier of 1L; ::_thesis: FinMeet ((f .: B),g) = FinMeet (B,(g * f)) set M = the L_meet of 1L; thus FinMeet ((f .: B),g) = the L_meet of 1L \$\$ ((f .: B),g) by LATTICE2:def_4 .= the L_meet of 1L \$\$ (B,(g * f)) by SETWISEO:35 .= FinMeet (B,(g * f)) by LATTICE2:def_4 ; ::_thesis: verum end; theorem Th23: :: LATTICE4:23 for 1L being upper-bounded Lattice for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2) proof let 1L be upper-bounded Lattice; ::_thesis: for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2) let B1, B2 be Finite_Subset of the carrier of 1L; ::_thesis: (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2) set M = the L_meet of 1L; thus FinMeet (B1 \/ B2) = the L_meet of 1L \$\$ ((B1 \/ B2),(id 1L)) by LATTICE2:def_4 .= ( the L_meet of 1L \$\$ (B1,(id 1L))) "/\" ( the L_meet of 1L \$\$ (B2,(id 1L))) by SETWISEO:33 .= (FinMeet B1) "/\" ( the L_meet of 1L \$\$ (B2,(id 1L))) by LATTICE2:def_4 .= (FinMeet B1) "/\" (FinMeet B2) by LATTICE2:def_4 ; ::_thesis: verum end; theorem Th24: :: LATTICE4:24 for 1L being upper-bounded Lattice for F being ClosedSubset of 1L st Top 1L in F holds for B being Finite_Subset of the carrier of 1L st B c= F holds FinMeet B in F proof let 1L be upper-bounded Lattice; ::_thesis: for F being ClosedSubset of 1L st Top 1L in F holds for B being Finite_Subset of the carrier of 1L st B c= F holds FinMeet B in F let F be ClosedSubset of 1L; ::_thesis: ( Top 1L in F implies for B being Finite_Subset of the carrier of 1L st B c= F holds FinMeet B in F ) defpred S1[ Finite_Subset of the carrier of 1L] means ( \$1 c= F implies FinMeet \$1 in F ); A1: for B1 being Finite_Subset of the carrier of 1L for p being Element of 1L st S1[B1] holds S1[B1 \/ {.p.}] proof let B1 be Finite_Subset of the carrier of 1L; ::_thesis: for p being Element of 1L st S1[B1] holds S1[B1 \/ {.p.}] let p be Element of 1L; ::_thesis: ( S1[B1] implies S1[B1 \/ {.p.}] ) assume A2: ( B1 c= F implies FinMeet B1 in F ) ; ::_thesis: S1[B1 \/ {.p.}] assume A3: B1 \/ {p} c= F ; ::_thesis: FinMeet (B1 \/ {.p.}) in F then {p} c= F by XBOOLE_1:11; then p in F by ZFMISC_1:31; then (FinMeet B1) "/\" p in F by A2, A3, LATTICES:def_24, XBOOLE_1:11; hence FinMeet (B1 \/ {.p.}) in F by Th21; ::_thesis: verum end; assume Top 1L in F ; ::_thesis: for B being Finite_Subset of the carrier of 1L st B c= F holds FinMeet B in F then A4: S1[ {}. the carrier of 1L] by Lm2; thus for B being Element of Fin the carrier of 1L holds S1[B] from SETWISEO:sch_4(A4, A1); ::_thesis: verum end; begin Lm3: for DL being distributive upper-bounded Lattice for B being Finite_Subset of the carrier of DL for p being Element of DL for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) proof let DL be distributive upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of DL for p being Element of DL for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) let B be Finite_Subset of the carrier of DL; ::_thesis: for p being Element of DL for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) let p be Element of DL; ::_thesis: for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) let f be UnOp of the carrier of DL; ::_thesis: the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) set J = the L_join of DL; set M = the L_meet of DL; now__::_thesis:_the_L_join_of_DL_._((_the_L_meet_of_DL_\$\$_(B,f)),p)_=_the_L_meet_of_DL_\$\$_(B,(_the_L_join_of_DL_[:]_(f,p))) percases ( B <> {} or B = {} ) ; suppose B <> {} ; ::_thesis: the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) hence the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) by LATTICE2:21, SETWISEO:28; ::_thesis: verum end; supposeA1: B = {} ; ::_thesis: the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) A2: now__::_thesis:_for_f_being_UnOp_of_the_carrier_of_DL_holds_the_L_meet_of_DL_\$\$_(B,f)_=_Top_DL let f be UnOp of the carrier of DL; ::_thesis: the L_meet of DL \$\$ (B,f) = Top DL thus the L_meet of DL \$\$ (B,f) = FinMeet (({}. the carrier of DL),f) by A1, LATTICE2:def_4 .= Top DL by Lm2 ; ::_thesis: verum end; hence the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = (Top DL) "\/" p .= Top DL .= the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) by A2 ; ::_thesis: verum end; end; end; hence the L_join of DL . (( the L_meet of DL \$\$ (B,f)),p) = the L_meet of DL \$\$ (B,( the L_join of DL [:] (f,p))) ; ::_thesis: verum end; theorem Th25: :: LATTICE4:25 for DL being distributive upper-bounded Lattice for B being Finite_Subset of the carrier of DL for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) proof let DL be distributive upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of DL for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) let B be Finite_Subset of the carrier of DL; ::_thesis: for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) let p be Element of DL; ::_thesis: (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) set J = the L_join of DL; set M = the L_meet of DL; thus (FinMeet B) "\/" p = the L_join of DL . (( the L_meet of DL \$\$ (B,(id DL))),p) by LATTICE2:def_4 .= the L_meet of DL \$\$ (B,( the L_join of DL [:] ((id DL),p))) by Lm3 .= FinMeet (B,( the L_join of DL [:] ((id DL),p))) by LATTICE2:def_4 .= FinMeet (B,((id DL) * ( the L_join of DL [:] ((id DL),p)))) by FUNCT_2:17 .= FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) by Th22 ; ::_thesis: verum end; begin theorem Th26: :: LATTICE4:26 for CL being C_Lattice for IL being implicative Lattice for f being Homomorphism of IL,CL for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j proof let CL be C_Lattice; ::_thesis: for IL being implicative Lattice for f being Homomorphism of IL,CL for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j let f be Homomorphism of IL,CL; ::_thesis: for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j let i, j be Element of IL; ::_thesis: (f . i) "/\" (f . (i => j)) [= f . j i "/\" (i => j) [= j by FILTER_0:def_7; then f . (i "/\" (i => j)) [= f . j by Th4; hence (f . i) "/\" (f . (i => j)) [= f . j by Def1; ::_thesis: verum end; theorem Th27: :: LATTICE4:27 for CL being C_Lattice for IL being implicative Lattice for f being Homomorphism of IL,CL for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds f . k [= f . (i => j) proof let CL be C_Lattice; ::_thesis: for IL being implicative Lattice for f being Homomorphism of IL,CL for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds f . k [= f . (i => j) let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds f . k [= f . (i => j) let f be Homomorphism of IL,CL; ::_thesis: for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds f . k [= f . (i => j) let i, k, j be Element of IL; ::_thesis: ( f is one-to-one & (f . i) "/\" (f . k) [= f . j implies f . k [= f . (i => j) ) assume A1: f is one-to-one ; ::_thesis: ( not (f . i) "/\" (f . k) [= f . j or f . k [= f . (i => j) ) hereby ::_thesis: verum assume (f . i) "/\" (f . k) [= f . j ; ::_thesis: f . k [= f . (i => j) then f . (i "/\" k) [= f . j by Def1; then i "/\" k [= j by A1, Th5; then k [= i => j by FILTER_0:def_7; hence f . k [= f . (i => j) by Th4; ::_thesis: verum end; end; theorem :: LATTICE4:28 for CL being C_Lattice for IL being implicative Lattice for f being Homomorphism of IL,CL st f is bijective holds ( CL is implicative & f preserves_implication ) proof let CL be C_Lattice; ::_thesis: for IL being implicative Lattice for f being Homomorphism of IL,CL st f is bijective holds ( CL is implicative & f preserves_implication ) let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL st f is bijective holds ( CL is implicative & f preserves_implication ) let f be Homomorphism of IL,CL; ::_thesis: ( f is bijective implies ( CL is implicative & f preserves_implication ) ) assume A1: f is bijective ; ::_thesis: ( CL is implicative & f preserves_implication ) thus CL is implicative ::_thesis: f preserves_implication proof let p, q be Element of CL; :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of CL st ( p "/\" b1 [= q & ( for b2 being Element of the carrier of CL holds ( not p "/\" b2 [= q or b2 [= b1 ) ) ) consider i being Element of IL such that A2: f . i = p by A1, Th6; consider j being Element of IL such that A3: f . j = q by A1, Th6; take r = f . (i => j); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of CL holds ( not p "/\" b1 [= q or b1 [= r ) ) ) thus p "/\" r [= q by A2, A3, Th26; ::_thesis: for b1 being Element of the carrier of CL holds ( not p "/\" b1 [= q or b1 [= r ) hereby ::_thesis: verum let r1 be Element of CL; ::_thesis: ( p "/\" r1 [= q implies r1 [= r ) assume A4: p "/\" r1 [= q ; ::_thesis: r1 [= r ex k being Element of IL st f . k = r1 by A1, Th6; hence r1 [= r by A1, A2, A3, A4, Th27; ::_thesis: verum end; end; then reconsider CL = CL as implicative Lattice ; reconsider f = f as Homomorphism of IL,CL ; now__::_thesis:_for_i,_j_being_Element_of_IL_holds_(f_._i)_=>_(f_._j)_=_f_._(i_=>_j) let i, j be Element of IL; ::_thesis: (f . i) => (f . j) = f . (i => j) A5: now__::_thesis:_for_r1_being_Element_of_CL_st_(f_._i)_"/\"_r1_[=_f_._j_holds_ r1_[=_f_._(i_=>_j) let r1 be Element of CL; ::_thesis: ( (f . i) "/\" r1 [= f . j implies r1 [= f . (i => j) ) assume A6: (f . i) "/\" r1 [= f . j ; ::_thesis: r1 [= f . (i => j) ex k being Element of IL st f . k = r1 by A1, Th6; hence r1 [= f . (i => j) by A1, A6, Th27; ::_thesis: verum end; (f . i) "/\" (f . (i => j)) [= f . j by Th26; hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def_7; ::_thesis: verum end; hence f preserves_implication by Def3; ::_thesis: verum end; begin theorem Th29: :: LATTICE4:29 for BL being Boolean Lattice holds (Top BL) ` = Bottom BL proof let BL be Boolean Lattice; ::_thesis: (Top BL) ` = Bottom BL set a = Bottom BL; thus (Top BL) ` = ((Bottom BL) "\/" ((Bottom BL) `)) ` by LATTICES:21 .= ((Bottom BL) `) "/\" (((Bottom BL) `) `) .= Bottom BL ; ::_thesis: verum end; theorem Th30: :: LATTICE4:30 for BL being Boolean Lattice holds (Bottom BL) ` = Top BL proof let BL be Boolean Lattice; ::_thesis: (Bottom BL) ` = Top BL set a = Top BL; thus (Bottom BL) ` = ((Top BL) "/\" ((Top BL) `)) ` by LATTICES:20 .= ((Top BL) `) "\/" (((Top BL) `) `) .= Top BL ; ::_thesis: verum end; theorem :: LATTICE4:31 for CL being C_Lattice for BL being Boolean Lattice for f being Homomorphism of BL,CL st f is onto holds ( CL is Boolean & f preserves_complement ) proof let CL be C_Lattice; ::_thesis: for BL being Boolean Lattice for f being Homomorphism of BL,CL st f is onto holds ( CL is Boolean & f preserves_complement ) let BL be Boolean Lattice; ::_thesis: for f being Homomorphism of BL,CL st f is onto holds ( CL is Boolean & f preserves_complement ) let f be Homomorphism of BL,CL; ::_thesis: ( f is onto implies ( CL is Boolean & f preserves_complement ) ) assume A1: f is onto ; ::_thesis: ( CL is Boolean & f preserves_complement ) then A2: f preserves_top by Th18; thus ( CL is bounded & CL is complemented ) ; :: according to LATTICES:def_20 ::_thesis: ( CL is distributive & f preserves_complement ) thus CL is distributive by A1, Th11; ::_thesis: f preserves_complement then reconsider CL = CL as Boolean Lattice ; A3: f preserves_bottom by A1, Th12; reconsider f = f as Homomorphism of BL,CL ; now__::_thesis:_for_a1_being_Element_of_BL_holds_(f_._a1)_`_=_f_._(a1_`) let a1 be Element of BL; ::_thesis: (f . a1) ` = f . (a1 `) A4: (f . (a1 `)) "/\" (f . a1) = f . ((a1 `) "/\" a1) by Def1 .= f . (Bottom BL) by LATTICES:20 .= Bottom CL by A3, Def5 ; (f . (a1 `)) "\/" (f . a1) = f . ((a1 `) "\/" a1) by Def1 .= f . (Top BL) by LATTICES:21 .= Top CL by A2, Def4 ; then f . (a1 `) is_a_complement_of f . a1 by A4, LATTICES:def_18; hence (f . a1) ` = f . (a1 `) by LATTICES:def_21; ::_thesis: verum end; hence f preserves_complement by Def6; ::_thesis: verum end; definition let BL be Boolean Lattice; mode Field of BL -> non empty Subset of BL means :Def9: :: LATTICE4:def 9 for a, b being Element of BL st a in it & b in it holds ( a "/\" b in it & a ` in it ); existence ex b1 being non empty Subset of BL st for a, b being Element of BL st a in b1 & b in b1 holds ( a "/\" b in b1 & a ` in b1 ) proof the carrier of BL c= the carrier of BL ; then reconsider F = the carrier of BL as non empty Subset of BL ; take F ; ::_thesis: for a, b being Element of BL st a in F & b in F holds ( a "/\" b in F & a ` in F ) thus for a, b being Element of BL st a in F & b in F holds ( a "/\" b in F & a ` in F ) ; ::_thesis: verum end; end; :: deftheorem Def9 defines Field LATTICE4:def_9_:_ for BL being Boolean Lattice for b2 being non empty Subset of BL holds ( b2 is Field of BL iff for a, b being Element of BL st a in b2 & b in b2 holds ( a "/\" b in b2 & a ` in b2 ) ); theorem Th32: :: LATTICE4:32 for BL being Boolean Lattice for a, b being Element of BL for F being Field of BL st a in F & b in F holds a "\/" b in F proof let BL be Boolean Lattice; ::_thesis: for a, b being Element of BL for F being Field of BL st a in F & b in F holds a "\/" b in F let a, b be Element of BL; ::_thesis: for F being Field of BL st a in F & b in F holds a "\/" b in F let F be Field of BL; ::_thesis: ( a in F & b in F implies a "\/" b in F ) assume ( a in F & b in F ) ; ::_thesis: a "\/" b in F then ( a ` in F & b ` in F ) by Def9; then (a `) "/\" (b `) in F by Def9; then (a "\/" b) ` in F by LATTICES:24; then ((a "\/" b) `) ` in F by Def9; hence a "\/" b in F by LATTICES:22; ::_thesis: verum end; theorem Th33: :: LATTICE4:33 for BL being Boolean Lattice for a, b being Element of BL for F being Field of BL st a in F & b in F holds a => b in F proof let BL be Boolean Lattice; ::_thesis: for a, b being Element of BL for F being Field of BL st a in F & b in F holds a => b in F let a, b be Element of BL; ::_thesis: for F being Field of BL st a in F & b in F holds a => b in F let F be Field of BL; ::_thesis: ( a in F & b in F implies a => b in F ) assume that A1: a in F and A2: b in F ; ::_thesis: a => b in F a ` in F by A1, Def9; then (a `) "\/" b in F by A2, Th32; hence a => b in F by FILTER_0:42; ::_thesis: verum end; theorem Th34: :: LATTICE4:34 for BL being Boolean Lattice holds the carrier of BL is Field of BL proof let BL be Boolean Lattice; ::_thesis: the carrier of BL is Field of BL the carrier of BL c= the carrier of BL ; then reconsider F = the carrier of BL as non empty Subset of BL ; for a, b being Element of BL st a in F & b in F holds ( a "/\" b in F & a ` in F ) ; hence the carrier of BL is Field of BL by Def9; ::_thesis: verum end; theorem Th35: :: LATTICE4:35 for BL being Boolean Lattice for F being Field of BL holds F is ClosedSubset of BL proof let BL be Boolean Lattice; ::_thesis: for F being Field of BL holds F is ClosedSubset of BL let F be Field of BL; ::_thesis: F is ClosedSubset of BL A1: for a, b being Element of BL st a in F & b in F holds a "/\" b in F by Def9; for a, b being Element of BL st a in F & b in F holds a "\/" b in F by Th32; hence F is ClosedSubset of BL by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum end; definition let BL be Boolean Lattice; let A be non empty Subset of BL; func field_by A -> Field of BL means :Def10: :: LATTICE4:def 10 ( A c= it & ( for F being Field of BL st A c= F holds it c= F ) ); existence ex b1 being Field of BL st ( A c= b1 & ( for F being Field of BL st A c= F holds b1 c= F ) ) proof set x = the Element of A; defpred S1[ set ] means ( \$1 is Field of BL & A c= \$1 ); consider X being set such that A1: for Z being set holds ( Z in X iff ( Z in bool the carrier of BL & S1[Z] ) ) from XBOOLE_0:sch_1(); reconsider x = the Element of A as Element of BL ; A2: the carrier of BL is Field of BL by Th34; then A3: X <> {} by A1; now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_ x_in_Z let Z be set ; ::_thesis: ( Z in X implies x in Z ) assume Z in X ; ::_thesis: x in Z then A c= Z by A1; hence x in Z by TARSKI:def_3; ::_thesis: verum end; then reconsider F1 = meet X as non empty set by A3, SETFAM_1:def_1; A4: the carrier of BL in X by A1, A2; F1 c= the carrier of BL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1 or x in the carrier of BL ) thus ( not x in F1 or x in the carrier of BL ) by A4, SETFAM_1:def_1; ::_thesis: verum end; then reconsider F1 = F1 as non empty Subset of BL ; F1 is Field of BL proof let a be Element of BL; :: according to LATTICE4:def_9 ::_thesis: for b being Element of BL st a in F1 & b in F1 holds ( a "/\" b in F1 & a ` in F1 ) let b be Element of BL; ::_thesis: ( a in F1 & b in F1 implies ( a "/\" b in F1 & a ` in F1 ) ) assume that A5: a in F1 and A6: b in F1 ; ::_thesis: ( a "/\" b in F1 & a ` in F1 ) A7: for Z being set st Z in X holds a "/\" b in Z proof let Z be set ; ::_thesis: ( Z in X implies a "/\" b in Z ) assume A8: Z in X ; ::_thesis: a "/\" b in Z then A9: b in Z by A6, SETFAM_1:def_1; ( Z is Field of BL & a in Z ) by A1, A5, A8, SETFAM_1:def_1; hence a "/\" b in Z by A9, Def9; ::_thesis: verum end; for Z being set st Z in X holds a ` in Z proof let Z be set ; ::_thesis: ( Z in X implies a ` in Z ) assume Z in X ; ::_thesis: a ` in Z then ( Z is Field of BL & a in Z ) by A1, A5, SETFAM_1:def_1; hence a ` in Z by Def9; ::_thesis: verum end; hence ( a "/\" b in F1 & a ` in F1 ) by A3, A7, SETFAM_1:def_1; ::_thesis: verum end; then reconsider F = F1 as Field of BL ; take F ; ::_thesis: ( A c= F & ( for F being Field of BL st A c= F holds F c= F ) ) for Z being set st Z in X holds A c= Z by A1; hence A c= F by A4, SETFAM_1:5; ::_thesis: for F being Field of BL st A c= F holds F c= F let H be Field of BL; ::_thesis: ( A c= H implies F c= H ) assume A c= H ; ::_thesis: F c= H then H in X by A1; hence F c= H by SETFAM_1:3; ::_thesis: verum end; uniqueness for b1, b2 being Field of BL st A c= b1 & ( for F being Field of BL st A c= F holds b1 c= F ) & A c= b2 & ( for F being Field of BL st A c= F holds b2 c= F ) holds b1 = b2 proof let F1, F2 be Field of BL; ::_thesis: ( A c= F1 & ( for F being Field of BL st A c= F holds F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds F2 c= F ) implies F1 = F2 ) assume ( A c= F1 & ( for F being Field of BL st A c= F holds F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds F2 c= F ) ) ; ::_thesis: F1 = F2 hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum end; end; :: deftheorem Def10 defines field_by LATTICE4:def_10_:_ for BL being Boolean Lattice for A being non empty Subset of BL for b3 being Field of BL holds ( b3 = field_by A iff ( A c= b3 & ( for F being Field of BL st A c= F holds b3 c= F ) ) ); definition let BL be Boolean Lattice; let A be non empty Subset of BL; func SetImp A -> Subset of BL equals :: LATTICE4:def 11 { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; coherence { (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL proof set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; { (a => b) where a, b is Element of BL : ( a in A & b in A ) } c= the carrier of BL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } or x in the carrier of BL ) assume x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; ::_thesis: x in the carrier of BL then ex p, q being Element of BL st ( x = p => q & p in A & q in A ) ; hence x in the carrier of BL ; ::_thesis: verum end; hence { (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL ; ::_thesis: verum end; end; :: deftheorem defines SetImp LATTICE4:def_11_:_ for BL being Boolean Lattice for A being non empty Subset of BL holds SetImp A = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; registration let BL be Boolean Lattice; let A be non empty Subset of BL; cluster SetImp A -> non empty ; coherence not SetImp A is empty proof set x = the Element of A; set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; reconsider x = the Element of A as Element of BL ; x => x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; then reconsider B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } as non empty set ; B = SetImp A ; hence not SetImp A is empty ; ::_thesis: verum end; end; theorem :: LATTICE4:36 for x being set for BL being Boolean Lattice for A being non empty Subset of BL holds ( x in SetImp A iff ex p, q being Element of BL st ( x = p => q & p in A & q in A ) ) ; theorem Th37: :: LATTICE4:37 for BL being Boolean Lattice for A being non empty Subset of BL for c being Element of BL holds ( c in SetImp A iff ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) ) proof let BL be Boolean Lattice; ::_thesis: for A being non empty Subset of BL for c being Element of BL holds ( c in SetImp A iff ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) ) let A be non empty Subset of BL; ::_thesis: for c being Element of BL holds ( c in SetImp A iff ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) ) let c be Element of BL; ::_thesis: ( c in SetImp A iff ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) ) hereby ::_thesis: ( ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) implies c in SetImp A ) assume c in SetImp A ; ::_thesis: ex p, q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) then consider p, q being Element of BL such that A1: ( c = p => q & p in A & q in A ) ; take p = p; ::_thesis: ex q being Element of BL st ( c = (p `) "\/" q & p in A & q in A ) take q = q; ::_thesis: ( c = (p `) "\/" q & p in A & q in A ) thus ( c = (p `) "\/" q & p in A & q in A ) by A1, FILTER_0:42; ::_thesis: verum end; given p, q being Element of BL such that A2: c = (p `) "\/" q and A3: ( p in A & q in A ) ; ::_thesis: c in SetImp A c = p => q by A2, FILTER_0:42; hence c in SetImp A by A3; ::_thesis: verum end; definition let BL be Boolean Lattice; deffunc H1( Element of BL) -> Element of the carrier of BL = \$1 ` ; func comp BL -> Function of the carrier of BL, the carrier of BL means :Def12: :: LATTICE4:def 12 for a being Element of BL holds it . a = a ` ; existence ex b1 being Function of the carrier of BL, the carrier of BL st for a being Element of BL holds b1 . a = a ` proof consider f being Function of the carrier of BL, the carrier of BL such that A1: for a being Element of BL holds f . a = H1(a) from FUNCT_2:sch_4(); take f ; ::_thesis: for a being Element of BL holds f . a = a ` thus for a being Element of BL holds f . a = a ` by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of BL, the carrier of BL st ( for a being Element of BL holds b1 . a = a ` ) & ( for a being Element of BL holds b2 . a = a ` ) holds b1 = b2 proof thus for f1, f2 being Function of the carrier of BL, the carrier of BL st ( for x being Element of BL holds f1 . x = H1(x) ) & ( for x being Element of BL holds f2 . x = H1(x) ) holds f1 = f2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def12 defines comp LATTICE4:def_12_:_ for BL being Boolean Lattice for b2 being Function of the carrier of BL, the carrier of BL holds ( b2 = comp BL iff for a being Element of BL holds b2 . a = a ` ); theorem Th38: :: LATTICE4:38 for BL being Boolean Lattice for b being Element of BL for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `) proof let BL be Boolean Lattice; ::_thesis: for b being Element of BL for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `) let b be Element of BL; ::_thesis: for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `) let B be Finite_Subset of the carrier of BL; ::_thesis: FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `) thus FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" ((comp BL) . b) by Th13 .= (FinJoin (B,(comp BL))) "\/" (b `) by Def12 ; ::_thesis: verum end; theorem :: LATTICE4:39 for BL being Boolean Lattice for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL)) proof let BL be Boolean Lattice; ::_thesis: for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL)) let B be Finite_Subset of the carrier of BL; ::_thesis: (FinJoin B) ` = FinMeet (B,(comp BL)) set M = the L_meet of BL; set J = the L_join of BL; A1: for a, b being Element of BL holds (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b)) proof let a, b be Element of BL; ::_thesis: (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b)) thus (comp BL) . ( the L_join of BL . (a,b)) = (a "\/" b) ` by Def12 .= (a `) "/\" (b `) by LATTICES:24 .= the L_meet of BL . (((comp BL) . a),(b `)) by Def12 .= the L_meet of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; ::_thesis: verum end; A2: (comp BL) . (the_unity_wrt the L_join of BL) = (the_unity_wrt the L_join of BL) ` by Def12 .= (Bottom BL) ` by LATTICE2:52 .= Top BL by Th30 .= the_unity_wrt the L_meet of BL by LATTICE2:57 ; thus (FinJoin B) ` = ( the L_join of BL \$\$ (B,(id BL))) ` by LATTICE2:def_3 .= (comp BL) . ( the L_join of BL \$\$ (B,(id BL))) by Def12 .= the L_meet of BL \$\$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36 .= the L_meet of BL \$\$ (B,(comp BL)) by FUNCT_2:17 .= FinMeet (B,(comp BL)) by LATTICE2:def_4 ; ::_thesis: verum end; theorem :: LATTICE4:40 for BL being Boolean Lattice for b being Element of BL for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `) proof let BL be Boolean Lattice; ::_thesis: for b being Element of BL for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `) let b be Element of BL; ::_thesis: for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `) let B be Finite_Subset of the carrier of BL; ::_thesis: FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `) thus FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" ((comp BL) . b) by Th20 .= (FinMeet (B,(comp BL))) "/\" (b `) by Def12 ; ::_thesis: verum end; theorem Th41: :: LATTICE4:41 for BL being Boolean Lattice for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL)) proof let BL be Boolean Lattice; ::_thesis: for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL)) let B be Finite_Subset of the carrier of BL; ::_thesis: (FinMeet B) ` = FinJoin (B,(comp BL)) set M = the L_meet of BL; set J = the L_join of BL; A1: for a, b being Element of BL holds (comp BL) . ( the L_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b)) proof let a, b be Element of BL; ::_thesis: (comp BL) . ( the L_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b)) thus (comp BL) . ( the L_meet of BL . (a,b)) = (a "/\" b) ` by Def12 .= (a `) "\/" (b `) by LATTICES:23 .= the L_join of BL . (((comp BL) . a),(b `)) by Def12 .= the L_join of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; ::_thesis: verum end; A2: (comp BL) . (the_unity_wrt the L_meet of BL) = (the_unity_wrt the L_meet of BL) ` by Def12 .= (Top BL) ` by LATTICE2:57 .= Bottom BL by Th29 .= the_unity_wrt the L_join of BL by LATTICE2:52 ; thus (FinMeet B) ` = ( the L_meet of BL \$\$ (B,(id BL))) ` by LATTICE2:def_4 .= (comp BL) . ( the L_meet of BL \$\$ (B,(id BL))) by Def12 .= the L_join of BL \$\$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36 .= the L_join of BL \$\$ (B,(comp BL)) by FUNCT_2:17 .= FinJoin (B,(comp BL)) by LATTICE2:def_3 ; ::_thesis: verum end; theorem Th42: :: LATTICE4:42 for BL being Boolean Lattice for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) proof let BL be Boolean Lattice; ::_thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) let AF be non empty ClosedSubset of BL; ::_thesis: ( Bottom BL in AF & Top BL in AF implies for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) ) assume that A1: Bottom BL in AF and A2: Top BL in AF ; ::_thesis: for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) set C = { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; A3: { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } or x in SetImp AF ) assume x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: x in SetImp AF then consider A1, A2 being Finite_Subset of the carrier of BL such that A4: x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and A5: ( A1 c= AF & A2 c= AF ) ; consider p, q being Element of BL such that A6: ( p = FinMeet A2 & q = FinJoin A1 ) ; A7: x = (p `) "\/" q by A4, A6, Th41; ( p in AF & q in AF ) by A1, A2, A5, A6, Th17, Th24; hence x in SetImp AF by A7, Th37; ::_thesis: verum end; defpred S1[ Finite_Subset of the carrier of BL] means ( \$1 c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (\$1,(comp BL)) = FinMeet B0 ) ); let B be Finite_Subset of the carrier of BL; ::_thesis: ( B c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) ) assume A8: B c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) A9: for B9 being Finite_Subset of the carrier of BL for b being Element of BL st S1[B9] holds S1[B9 \/ {.b.}] proof set J = the L_join of BL; let B9 be Finite_Subset of the carrier of BL; ::_thesis: for b being Element of BL st S1[B9] holds S1[B9 \/ {.b.}] let b be Element of BL; ::_thesis: ( S1[B9] implies S1[B9 \/ {.b.}] ) assume A10: ( B9 c= SetImp AF implies ex B1 being Finite_Subset of the carrier of BL st ( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B9,(comp BL)) = FinMeet B1 ) ) ; ::_thesis: S1[B9 \/ {.b.}] assume A11: B9 \/ {b} c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet B0 ) then consider B1 being Finite_Subset of the carrier of BL such that A12: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } and A13: FinJoin (B9,(comp BL)) = FinMeet B1 by A10, ZFMISC_1:137; b in SetImp AF by A11, ZFMISC_1:137; then consider p, q being Element of BL such that A14: b = (p `) "\/" q and A15: p in AF and A16: q in AF by Th37; A17: for x being set for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds ex a being Element of BL st ( a in B1 & x = a "\/" b ) proof let x be set ; ::_thesis: for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds ex a being Element of BL st ( a in B1 & x = a "\/" b ) let b be Element of BL; ::_thesis: ( x in ( the L_join of BL [:] ((id BL),b)) .: B1 implies ex a being Element of BL st ( a in B1 & x = a "\/" b ) ) assume A18: x in ( the L_join of BL [:] ((id BL),b)) .: B1 ; ::_thesis: ex a being Element of BL st ( a in B1 & x = a "\/" b ) ( the L_join of BL [:] ((id BL),b)) .: B1 c= the carrier of BL by FUNCT_2:36; then reconsider x = x as Element of BL by A18; consider a being Element of BL such that A19: a in B1 and A20: x = ( the L_join of BL [:] ((id BL),b)) . a by A18, FUNCT_2:65; x = the L_join of BL . (((id BL) . a),b) by A20, FUNCOP_1:48 .= a "\/" b by FUNCT_1:18 ; hence ex a being Element of BL st ( a in B1 & x = a "\/" b ) by A19; ::_thesis: verum end; A21: ( the L_join of BL [:] ((id BL),p)) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( the L_join of BL [:] ((id BL),p)) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ) assume x in ( the L_join of BL [:] ((id BL),p)) .: B1 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } then consider a being Element of BL such that A22: a in B1 and A23: x = a "\/" p by A17; a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A22; then consider A1, A2 being Finite_Subset of the carrier of BL such that A24: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and A25: ( A1 c= AF & A2 c= AF ) ; ex A19, A29 being Finite_Subset of the carrier of BL st ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) proof take A19 = A1 \/ {.p.}; ::_thesis: ex A29 being Finite_Subset of the carrier of BL st ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) take A29 = A2; ::_thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) x = ((FinJoin A1) "\/" p) "\/" (FinJoin (A2,(comp BL))) by A23, A24, LATTICES:def_5 .= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th14 ; hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A15, A25, ZFMISC_1:137; ::_thesis: verum end; hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum end; A26: ( the L_join of BL [:] ((id BL),(q `))) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ) assume x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } then consider a being Element of BL such that A27: a in B1 and A28: x = a "\/" (q `) by A17; a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A27; then consider A1, A2 being Finite_Subset of the carrier of BL such that A29: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and A30: ( A1 c= AF & A2 c= AF ) ; ex A19, A29 being Finite_Subset of the carrier of BL st ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) proof take A19 = A1; ::_thesis: ex A29 being Finite_Subset of the carrier of BL st ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) take A29 = A2 \/ {.q.}; ::_thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) x = (FinJoin A1) "\/" ((FinJoin (A2,(comp BL))) "\/" (q `)) by A28, A29, LATTICES:def_5 .= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th38 ; hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A16, A30, ZFMISC_1:137; ::_thesis: verum end; hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum end; take (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) ; ::_thesis: ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) b ` = ((p `) `) "/\" (q `) by A14, LATTICES:24 .= p "/\" (q `) ; then FinJoin ((B9 \/ {.b.}),(comp BL)) = (FinMeet B1) "\/" (p "/\" (q `)) by A13, Th38 .= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q `)) by LATTICES:11 .= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" ((FinMeet B1) "\/" (q `)) by Th25 .= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" (FinMeet (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th25 .= FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th23 ; hence ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) by A21, A26, XBOOLE_1:8; ::_thesis: verum end; A31: S1[ {}. the carrier of BL] proof assume {}. the carrier of BL c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) take B0 = {.(Bottom BL).}; ::_thesis: ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) A32: B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B0 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ) assume x in B0 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } then A33: x = Bottom BL by TARSKI:def_1; ex A1, A2 being Finite_Subset of the carrier of BL st ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF ) proof take A1 = {.(Bottom BL).}; ::_thesis: ex A2 being Finite_Subset of the carrier of BL st ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF ) take A2 = {.(Top BL).}; ::_thesis: ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF ) thus x = (Bottom BL) "\/" (Bottom BL) by A33 .= (Bottom BL) "\/" ((Top BL) `) by Th29 .= (FinJoin A1) "\/" ((Top BL) `) by Th9 .= (FinJoin A1) "\/" ((FinMeet A2) `) by Th10 .= (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) by Th41 ; ::_thesis: ( A1 c= AF & A2 c= AF ) thus A1 c= AF by A1, ZFMISC_1:31; ::_thesis: A2 c= AF thus A2 c= AF by A2, ZFMISC_1:31; ::_thesis: verum end; hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum end; FinJoin (({}. the carrier of BL),(comp BL)) = Bottom BL by Lm1 .= FinMeet {.(Bottom BL).} by Th10 ; hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) by A32; ::_thesis: verum end; for B being Finite_Subset of the carrier of BL holds S1[B] from SETWISEO:sch_4(A31, A9); then ex B1 being Finite_Subset of the carrier of BL st ( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B,(comp BL)) = FinMeet B1 ) by A8; hence ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) by A3, XBOOLE_1:1; ::_thesis: verum end; theorem :: LATTICE4:43 for BL being Boolean Lattice for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF proof let BL be Boolean Lattice; ::_thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF let AF be non empty ClosedSubset of BL; ::_thesis: ( Bottom BL in AF & Top BL in AF implies { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF ) assume that A1: Bottom BL in AF and A2: Top BL in AF ; ::_thesis: { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF set A1 = { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } ; A3: AF c= { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AF or x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } ) assume A4: x in AF ; ::_thesis: x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } then reconsider b = x as Element of BL ; reconsider B = {.b.} as Finite_Subset of the carrier of BL ; b = (Bottom BL) "\/" b .= ((Top BL) `) "\/" b by Th29 ; then b in SetImp AF by A2, A4, Th37; then A5: B c= SetImp AF by ZFMISC_1:31; x = FinMeet B by Th10; hence x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } by A5; ::_thesis: verum end; { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } c= the carrier of BL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } or x in the carrier of BL ) assume x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } ; ::_thesis: x in the carrier of BL then ex B being Finite_Subset of the carrier of BL st ( x = FinMeet B & B c= SetImp AF ) ; hence x in the carrier of BL ; ::_thesis: verum end; then reconsider A1 = { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } as non empty Subset of BL by A3; A6: now__::_thesis:_for_F_being_Field_of_BL_st_AF_c=_F_holds_ A1_c=_F let F be Field of BL; ::_thesis: ( AF c= F implies A1 c= F ) assume A7: AF c= F ; ::_thesis: A1 c= F thus A1 c= F ::_thesis: verum proof reconsider F1 = F as ClosedSubset of BL by Th35; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in F ) assume x in A1 ; ::_thesis: x in F then consider B being Finite_Subset of the carrier of BL such that A8: x = FinMeet B and A9: B c= SetImp AF ; SetImp AF c= F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in SetImp AF or y in F ) assume y in SetImp AF ; ::_thesis: y in F then ex p, q being Element of BL st ( y = p => q & p in AF & q in AF ) ; hence y in F by A7, Th33; ::_thesis: verum end; then B c= F1 by A9, XBOOLE_1:1; hence x in F by A2, A7, A8, Th24; ::_thesis: verum end; end; A1 is Field of BL proof let p be Element of BL; :: according to LATTICE4:def_9 ::_thesis: for b being Element of BL st p in A1 & b in A1 holds ( p "/\" b in A1 & p ` in A1 ) let q be Element of BL; ::_thesis: ( p in A1 & q in A1 implies ( p "/\" q in A1 & p ` in A1 ) ) assume that A10: p in A1 and A11: q in A1 ; ::_thesis: ( p "/\" q in A1 & p ` in A1 ) thus p "/\" q in A1 ::_thesis: p ` in A1 proof consider B2 being Finite_Subset of the carrier of BL such that A12: ( q = FinMeet B2 & B2 c= SetImp AF ) by A11; consider B1 being Finite_Subset of the carrier of BL such that A13: ( p = FinMeet B1 & B1 c= SetImp AF ) by A10; consider B0 being Finite_Subset of the carrier of BL such that A14: B0 = B1 \/ B2 ; ( B0 c= SetImp AF & p "/\" q = FinMeet B0 ) by A13, A12, A14, Th23, XBOOLE_1:8; hence p "/\" q in A1 ; ::_thesis: verum end; thus p ` in A1 ::_thesis: verum proof consider B being Finite_Subset of the carrier of BL such that A15: p = FinMeet B and A16: B c= SetImp AF by A10; p ` = FinJoin (B,(comp BL)) by A15, Th41; then ex B0 being Finite_Subset of the carrier of BL st ( B0 c= SetImp AF & p ` = FinMeet B0 ) by A1, A2, A16, Th42; hence p ` in A1 ; ::_thesis: verum end; end; hence { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF by A3, A6, Def10; ::_thesis: verum end;