:: deftheorem defines additive MSSUBFAM:def 2 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A (\/) B in IT );