defpred S1[ set ] means ex C being Subalgebra of B st
( $1 = the carrier of C & A c= $1 );
consider X being Subset-Family of B such that
A1: for Y being Subset of B holds
( Y in X iff S1[Y] ) from SUBSET_1:sch 3();
A2: now :: thesis: for Y being set st Y in X holds
A c= Y
let Y be set ; :: thesis: ( Y in X implies A c= Y )
assume Y in X ; :: thesis: A c= Y
then ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) by A1;
hence A c= Y ; :: thesis: verum
end;
set M = meet X;
for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) by A1;
then A3: meet X is opers_closed by Th20;
then consider C being strict Subalgebra of B such that
A4: meet X = the carrier of C by Th19;
reconsider C = C as non empty strict Subalgebra of B by A3, A4;
take C ; :: thesis: ( A c= the carrier of C & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of C c= the carrier of C ) )
( B is Subalgebra of B & the carrier of B in bool the carrier of B ) by Th11, ZFMISC_1:def 1;
then X <> {} by A1;
hence A c= the carrier of C by A4, A2, SETFAM_1:5; :: thesis: for C being Subalgebra of B st A c= the carrier of C holds
the carrier of C c= the carrier of C
let C1 be Subalgebra of B; :: thesis: ( A c= the carrier of C1 implies the carrier of C c= the carrier of C1 )
assume A5: A c= the carrier of C1 ; :: thesis: the carrier of C c= the carrier of C1
the carrier of C1 c= the carrier of B by Def3;
then the carrier of C1 in X by A1, A5;
hence the carrier of C c= the carrier of C1 by A4, SETFAM_1:3; :: thesis: verum