set x = the Element of A;

defpred S_{1}[ 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 & S_{1}[Z] ) )
from XFAMILY: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;

A4: the carrier of BL in X by A1, A2;

F1 c= the carrier of BL by A4, SETFAM_1:def 1;

then reconsider F1 = F1 as non empty Subset of BL ;

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

defpred S

consider X being set such that

A1: for Z being set holds

( Z in X iff ( Z in bool the carrier of BL & S

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

then reconsider F1 = meet X as non empty set by A3, SETFAM_1:def 1;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 ; :: thesis: verum

end;assume Z in X ; :: thesis: x in Z

then A c= Z by A1;

hence x in Z ; :: thesis: verum

A4: the carrier of BL in X by A1, A2;

F1 c= the carrier of BL by A4, SETFAM_1:def 1;

then reconsider F1 = F1 as non empty Subset of BL ;

F1 is Field of BL

proof

then reconsider F = F1 as Field of BL ;
let a be Element of BL; :: according to LATTICE4:def 10 :: 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

a ` in Z

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

for Z being set st Z in X holds
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;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

a ` in Z

proof

hence
( a "/\" b in F1 & a ` in F1 )
by A3, A7, SETFAM_1:def 1; :: thesis: verum
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;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

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