:: deftheorem defines multiplicative CLOSURE2:def 6 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily 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 );