:: deftheorem Def8 defines properly-upper-bound CLOSURE2:def 8 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );