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
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;
bool Omega is MonotoneClass of Omega by Th68;
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
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 ) }
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
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
now :: thesis: for n being Nat holds MSeq . n in Z
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;
then A6: rng MSeq c= Z by NAT_1:52;
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;
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: 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, Th69, SETFAM_1:3;
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:3; :: 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 A2, A1, SETFAM_1:5; :: thesis: verum