set x = the Element of A;
defpred S₁[ 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₁[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;

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 A3, SETFAM_1:def 1;
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

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

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 A1, A5, SETFAM_1:def 1;
hence a ` in Z by Def9; :: thesis: verum

end;

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