let X, Z be set ; :: thesis: ( Z is MonotoneClass of X iff ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) )
thus ( Z is MonotoneClass of X implies ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) ) :: thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) implies Z is MonotoneClass of X )
proof
assume A1: Z is MonotoneClass of X ; :: thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) )
then reconsider Z = Z as Subset-Family of X ;
for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; :: thesis: ( A1 is monotone & rng A1 c= Z implies lim A1 in Z )
assume that
A2: A1 is monotone and
A3: rng A1 c= Z ; :: thesis: lim A1 in Z
per cases ( not A1 is V75() or not A1 is V74() ) by A2, SETLIM_1:def 1;
suppose A1 is V75() ; :: thesis: lim A1 in Z
hence lim A1 in Z by A1, A3, Th66; :: thesis: verum
end;
suppose A1 is V74() ; :: thesis: lim A1 in Z
hence lim A1 in Z by A1, A3, Th67; :: thesis: verum
end;
end;
end;
hence ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) ; :: thesis: verum
end;
assume that
A4: Z c= bool X and
A5: for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ; :: thesis: Z is MonotoneClass of X
reconsider Z = Z as Subset-Family of X by A4;
A6: for A1 being SetSequence of X st A1 is V74() & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; :: thesis: ( A1 is V74() & rng A1 c= Z implies lim A1 in Z )
assume A7: ( A1 is V74() & rng A1 c= Z ) ; :: thesis: lim A1 in Z
( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5;
hence lim A1 in Z by A7, SETLIM_1:def 1; :: thesis: verum
end;
for A1 being SetSequence of X st A1 is V75() & rng A1 c= Z holds
lim A1 in Z
proof
let A1 be SetSequence of X; :: thesis: ( A1 is V75() & rng A1 c= Z implies lim A1 in Z )
assume A8: ( A1 is V75() & rng A1 c= Z ) ; :: thesis: lim A1 in Z
( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5;
hence lim A1 in Z by A8, SETLIM_1:def 1; :: thesis: verum
end;
hence Z is MonotoneClass of X by A6, Th66, Th67; :: thesis: verum