let Omega be non empty set ; :: thesis: for X being Subset-Family of Omega ex Y being MonotoneClass of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) )
let X be Subset-Family of Omega; :: thesis: ex Y being MonotoneClass of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) )
set V = { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
set Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
A1: bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) }

proof

bool Omega is MonotoneClass of Omega by Th76;
hence bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: verum

end;

then A2: ( meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } c= bool Omega & { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } <> {} ) by SETFAM_1:4;
A3: for Z being set st Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds
X c= Z

proof

let Z be set ; :: thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies X c= Z )
assume Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: X c= Z
then ex M being Subset-Family of Omega st
( Z = M & X c= M & M is MonotoneClass of Omega ) ;
hence X c= Z ; :: thesis: verum

end;

for MSeq being SetSequence of Omega st MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds
lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) }

proof

let MSeq be SetSequence of Omega; :: thesis: ( MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } )
assume that
A4: MSeq is monotone and
A5: rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) }

now

let Z be set ; :: thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in Z )
assume A6: Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: lim MSeq in Z
then A7: ex M being Subset-Family of Omega st
( Z = M & X c= M & M is MonotoneClass of Omega ) ;

now

let n be Nat; :: thesis: MSeq . n in Z
MSeq . n in rng MSeq by NAT_1:52;
then MSeq . n in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } by A5;
hence MSeq . n in Z by A6, SETFAM_1:def 1; :: thesis: verum

end;

then rng MSeq c= Z by NAT_1:53;
hence lim MSeq in Z by A4, A7, Th74; :: thesis: verum

end;

hence lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } by A1, SETFAM_1:def 1; :: thesis: verum

end;

then reconsider Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } as MonotoneClass of Omega by A2, Th74;
take Y ; :: thesis: ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) )
for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z

proof

let Z be set ; :: thesis: ( X c= Z & Z is MonotoneClass of Omega implies Y c= Z )
assume ( X c= Z & Z is MonotoneClass of Omega ) ; :: thesis: Y c= Z
then Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;
hence Y c= Z by SETFAM_1:4; :: thesis: verum

end;

hence ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) ) by A1, A3, SETFAM_1:6; :: thesis: verum