:: deftheorem Def8 defines non-increasing-closed PROB_3:def 10 :
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
Intersection A1 in IT );