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 V74() & 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 V74() & 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 V74() & rng A1 c= IT holds
lim A1 in IT ) :: thesis: ( ( for A1 being SetSequence of X st A1 is V74() & 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 V74() & rng A1 c= IT holds
lim A1 in IT
now :: thesis: for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
lim A1 in IT
let A1 be SetSequence of X; :: thesis: ( A1 is V74() & rng A1 c= IT implies lim A1 in IT )
assume that
A2: A1 is V74() 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 V74() & rng A1 c= IT holds
lim A1 in IT ; :: thesis: verum
end;
assume A4: for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
lim A1 in IT ; :: thesis: IT is non-increasing-closed
for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
Intersection A1 in IT
proof
let A1 be SetSequence of X; :: thesis: ( A1 is V74() & rng A1 c= IT implies Intersection A1 in IT )
assume that
A5: A1 is V74() 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