for X being set
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 )