:: deftheorem Def20 defines addint BINOP_2:def 20 :
for b₁ being BinOp of INT holds
( b₁ = addint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 + i2 );