:: deftheorem Def5 defines additive CLOSURE1:def 5 :
for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is additive iff the Family of IT is additive );