:: deftheorem EXNDef defines ex123/\ LATWAL_1:def 9 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = ex123/\ iff for x, y being Element of {0,1,2} holds b₁ . (x,y) = x ex123"/\" y );