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 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 ; :: thesis: verum
end;
then reconsider F1 = meet X as non empty set by ;
A4: the carrier of BL in X by A1, A2;
F1 c= the carrier of BL by ;
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 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
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 ;
( Z is Field of BL & a in Z ) by ;
hence a "/\" b in Z by ; :: 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 ;
hence a ` in Z by Def9; :: thesis: verum
end;
hence ( a "/\" b in F1 & a ` in F1 ) by ; :: 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 ; :: 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