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