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 Element of Fin 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 Element of Fin 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 Element of Fin the carrier of BL : B c= SetImp AF } = field_by AF
set A1 = { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } ;
A3: AF c= { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in AF or x in { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } )
assume A4: x in AF ; :: thesis: x in { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF }
then reconsider b = x as Element of BL ;
reconsider B = {.b.} as Element of Fin 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 Element of Fin the carrier of BL : B c= SetImp AF } by A5; :: thesis: verum
end;
{ (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } c= the carrier of BL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } or x in the carrier of BL )
assume x in { (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } ; :: thesis: x in the carrier of BL
then ex B being Element of Fin 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 Element of Fin 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 object ; :: 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 Element of Fin the carrier of BL such that
A8: x = FinMeet B and
A9: B c= SetImp AF ;
SetImp AF c= F
proof
let y be object ; :: 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;
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 10 :: 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 Element of Fin the carrier of BL such that
A12: ( q = FinMeet B2 & B2 c= SetImp AF ) by A11;
consider B1 being Element of Fin the carrier of BL such that
A13: ( p = FinMeet B1 & B1 c= SetImp AF ) by A10;
consider B0 being Element of Fin 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 Element of Fin 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 Element of Fin 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 Element of Fin the carrier of BL : B c= SetImp AF } = field_by AF by A3, A6, Def10; :: thesis: verum