:: deftheorem defines lower-bounded TAXONOM2:def 7 :
for Y being set
for F being Subset-Family of Y holds
( F is lower-bounded iff for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B ) );