:: 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;