:: deftheorem defines properly-upper-bound MSSUBFAM:def 6 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );