:: deftheorem defines diffint BINOP_2:def 21 :
for b₁ being BinOp of INT holds
( b₁ = diffint iff for i1, i2 being Integer holds b₁ . (i1,i2) = i1 - i2 );