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