:: deftheorem Defx7 defines example33\/ LATTAD_1:def 21 :
for b₁ being BinOp of {1,2,3} holds
( b₁ = example33\/ iff for x, y being Element of {1,2,3} holds b₁ . (x,y) = x example33"\/" y );