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

proof

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

now :: thesis: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
lim A1 in IT

let A1 be SetSequence of X; :: thesis: ( A1 is non-ascending & rng A1 c= IT implies lim A1 in IT )
assume that
A2: A1 is non-ascending and
A3: rng A1 c= IT ; :: thesis: lim A1 in IT
Intersection A1 in IT by A1, A2, A3;
hence lim A1 in IT by A2, SETLIM_1:64; :: thesis: verum

end;

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

end;

assume A4: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
lim A1 in IT ; :: thesis: IT is non-increasing-closed
for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
Intersection A1 in IT

proof

let A1 be SetSequence of X; :: thesis: ( A1 is non-ascending & rng A1 c= IT implies Intersection A1 in IT )
assume that
A5: A1 is non-ascending and
A6: rng A1 c= IT ; :: thesis: Intersection A1 in IT
lim A1 in IT by A4, A5, A6;
hence Intersection A1 in IT by A5, SETLIM_1:64; :: thesis: verum

end;

hence IT is non-increasing-closed ; :: thesis: verum