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