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 }

{ (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

{ (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } c= the carrier of BL
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;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

proof

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

A6: now :: thesis: for F being Field of BL st AF c= F holds

A1 c= F

A1 is Field of BL
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

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

hence x in F by A2, A7, A8, Th24; :: thesis: verum

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

then
B c= F1
by A9;
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;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

hence x in F by A2, A7, A8, Th24; :: thesis: verum

proof

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

end;( 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

thus
p ` in A1
:: thesis: verum
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;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

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