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 A1: ( Bottom BL in AF & 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 } ;
A2: 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 A3: 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 by LATTICES:39
.= ((Top BL) ` ) "\/" b by Th36 ;
then b in SetImp AF by A1, A3, Th44;
then A4: B c= SetImp AF by ZFMISC_1:37;
x = FinMeet B by Th17;
hence x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } by A4; :: 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 consider B being Finite_Subset of the carrier of BL such that
A5: ( x = FinMeet B & B c= SetImp AF ) ;
thus x in the carrier of BL by A5; :: 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 A2;
A6: A1 is Field of BL

proof

let p be Element of BL; :: according to LATTICE4:def 14 :: 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 A7: ( p in A1 & q in A1 ) ; :: thesis: ( p "/\" q in A1 & p ` in A1 )
thus p "/\" q in A1 :: thesis: p ` in A1

proof

consider B1 being Finite_Subset of the carrier of BL such that
A8: ( p = FinMeet B1 & B1 c= SetImp AF ) by A7;
consider B2 being Finite_Subset of the carrier of BL such that
A9: ( q = FinMeet B2 & B2 c= SetImp AF ) by A7;
consider B0 being Finite_Subset of the carrier of BL such that
A10: B0 = B1 \/ B2 ;
A11: B0 c= SetImp AF by A8, A9, A10, XBOOLE_1:8;
p "/\" q = FinMeet B0 by A8, A9, A10, Th30;
hence p "/\" q in A1 by A11; :: thesis: verum

end;

thus p ` in A1 :: thesis: verum

proof

consider B being Finite_Subset of the carrier of BL such that
A12: ( p = FinMeet B & B c= SetImp AF ) by A7;
p ` = FinJoin B,(comp BL) by A12, Th48;
then consider B0 being Finite_Subset of the carrier of BL such that
A13: ( B0 c= SetImp AF & p ` = FinMeet B0 ) by A1, A12, Th49;
thus p ` in A1 by A13; :: thesis: verum

end;

end;

now

let F be Field of BL; :: thesis: ( AF c= F implies A1 c= F )
assume A14: AF c= F ; :: thesis: A1 c= F
thus A1 c= F :: thesis: verum

proof

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
A15: ( x = FinMeet B & B c= SetImp AF ) ;
A16: 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 consider p, q being Element of BL such that
A17: ( y = p => q & p in AF & q in AF ) ;
thus y in F by A14, A17, Th40; :: thesis: verum

end;

reconsider F1 = F as ClosedSubset of BL by Th42;
( B c= F1 & Top BL in F1 ) by A1, A14, A15, A16, XBOOLE_1:1;
hence x in F by A15, Th31; :: 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 A2, A6, Def15; :: thesis: verum