:: deftheorem EXUDef defines ex123\/ LATWAL_1:def 8 :
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 );