let Z, X 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 ;
A2: ( Z is non-decreasing-closed & Z is non-increasing-closed ) by A1;
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 A3: ( A1 is monotone & rng A1 c= Z ) ; :: thesis: lim A1 in Z

per cases ( A1 is non-descending or A1 is non-ascending ) by A3, SETLIM_1:def 1;

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

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

end;

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

hence lim A1 in Z by A2, A3, Th72; :: 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;
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 A6: ( 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 A6, SETLIM_1:def 1; :: thesis: verum

end;

then A7: Z is non-decreasing-closed by Th71;
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 A8: ( 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 A8, SETLIM_1:def 1; :: thesis: verum

end;

then Z is non-increasing-closed by Th72;
hence Z is MonotoneClass of X by A7; :: thesis: verum