:: deftheorem Defx8 defines example33/\ LATTAD_1:def 22 :
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 );