:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :
for L being non empty RelStr
for b₂ being Function of [:L,L:],L holds
( b₂ = sup_op L iff for x, y being Element of L holds b₂ . (x,y) = x "\/" y );