:: deftheorem Def16 defines multiplicative CLOSURE2:def 16 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );