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

then A2: bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;

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 ) }

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

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum

set Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;

A1: 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

bool Omega is MonotoneClass of Omega
by Th68;
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;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

then A2: bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ;

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

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, Th69, SETFAM_1:3;
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

A3: MSeq is monotone and

A4: 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 ) }

end;assume that

A3: MSeq is monotone and

A4: 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 :: thesis: for Z being set st Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds

lim MSeq in Z

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

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 A5: Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: lim MSeq in Z

ex M being Subset-Family of Omega st

( Z = M & X c= M & M is MonotoneClass of Omega ) by A5;

hence lim MSeq in Z by A3, A6, Th69; :: thesis: verum

end;assume A5: Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; :: thesis: lim MSeq in Z

now :: thesis: for n being Nat holds MSeq . n in Z

then A6:
rng MSeq c= Z
by NAT_1:52;let n be Nat; :: thesis: MSeq . n in Z

MSeq . n in rng MSeq by NAT_1:51;

hence MSeq . n in Z by A4, A5, SETFAM_1:def 1; :: thesis: verum

end;MSeq . n in rng MSeq by NAT_1:51;

hence MSeq . n in Z by A4, A5, SETFAM_1:def 1; :: thesis: verum

ex M being Subset-Family of Omega st

( Z = M & X c= M & M is MonotoneClass of Omega ) by A5;

hence lim MSeq in Z by A3, A6, Th69; :: thesis: verum

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

hence
( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
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:3; :: thesis: verum

end;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:3; :: thesis: verum

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum