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