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 non-descending or not A1 is non-ascending ) by A2, SETLIM_1:def 1;

suppose A1 is non-descending ; :: thesis: lim A1 in Z

hence lim A1 in Z by A1, A3, Th66; :: thesis: verum

end;

suppose A1 is non-ascending ; :: 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 non-ascending & rng A1 c= Z holds
lim A1 in Z

proof

let A1 be SetSequence of X; :: thesis: ( A1 is non-ascending & rng A1 c= Z implies lim A1 in Z )
assume A7: ( A1 is non-ascending & 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 non-descending & rng A1 c= Z holds
lim A1 in Z

proof

let A1 be SetSequence of X; :: thesis: ( A1 is non-descending & rng A1 c= Z implies lim A1 in Z )
assume A8: ( A1 is non-descending & 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