:: deftheorem Def14 defines additive CLOSURE2:def 14 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is additive iff the Family of IT is additive );