let X be set ; :: thesis: for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT )
let IT be Subset-Family of X; :: thesis: ( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT )
thus ( IT is non-decreasing-closed implies for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT ) :: thesis: ( ( for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT ) implies IT is non-decreasing-closed )

proof

assume A1: IT is non-decreasing-closed ; :: thesis: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT

now

let A1 be SetSequence of X; :: thesis: ( A1 is non-descending & rng A1 c= IT implies lim A1 in IT )
assume A2: ( A1 is non-descending & rng A1 c= IT ) ; :: thesis: lim A1 in IT
then Union A1 in IT by A1, Def12;
hence lim A1 in IT by A2, SETLIM_1:63; :: thesis: verum

end;

hence for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT ; :: thesis: verum

end;

assume A3: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT ; :: thesis: IT is non-decreasing-closed
for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
Union A1 in IT

proof

let A1 be SetSequence of X; :: thesis: ( A1 is non-descending & rng A1 c= IT implies Union A1 in IT )
assume A4: ( A1 is non-descending & rng A1 c= IT ) ; :: thesis: Union A1 in IT
then lim A1 in IT by A3;
hence Union A1 in IT by A4, SETLIM_1:63; :: thesis: verum

end;

hence IT is non-decreasing-closed by Def12; :: thesis: verum