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