:: deftheorem Def15 defines add3 MOD_2:def 15 :
for b₁ being BinOp of {0,1,2} holds
( b₁ = add3 iff for a, b being Element of {0,1,2} holds b₁ . (a,b) = a + b );