:: deftheorem Def10 defines with_suprema LATTICE3:def 10 :
for IT being RelStr holds
( IT is with_suprema iff for x, y being Element of IT ex z being Element of IT st
( x <= z & y <= z & ( for z9 being Element of IT st x <= z9 & y <= z9 holds
z <= z9 ) ) );