:: deftheorem defines lower-bounded' SHEFFER1:def 3 :
for IT being non empty LattStr holds
( IT is lower-bounded' iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a ) );