:: deftheorem Def18 defines properly-upper-bound CLOSURE2:def 18 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );