:: deftheorem Def9 defines properly-upper-bound CLOSURE1:def 9 :
for S being 1-sorted
for IT being MSClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );