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