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