:: deftheorem Def7 defines non-decreasing-closed PROB_3:def 9 :
for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V75() & rng A1 c= IT holds
Union A1 in IT );