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 )

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

lim A1 in Z

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

lim A1 in Z ) ) ; :: thesis: verum

end;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

hence
( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
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

end;assume that

A2: A1 is monotone and

A3: rng A1 c= Z ; :: thesis: lim A1 in Z

lim A1 in Z ) ) ; :: thesis: verum

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

for A1 being SetSequence of X st A1 is V75() & rng A1 c= Z holds
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;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

lim A1 in Z

proof

hence
Z is MonotoneClass of X
by A6, Th66, Th67; :: thesis: verum
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;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