:: deftheorem Defx7 defines example32\/ LATTAD_1:def 17 :
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 );