:: deftheorem Def7 defines multiplicative CLOSURE1:def 7 :
for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );