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