defpred S_{1}[ 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 S_{1}[Y] )
from SUBSET_1:sch 3();

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

( $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 S

A2: now :: thesis: for Y being set st Y in X holds

A c= Y

set M = meet X;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;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

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