:: deftheorem Def7 defines absolutely-multiplicative CLOSURE2:def 7 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT );