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