:: deftheorem defines diffreal BINOP_2:def 10 :
for b₁ being BinOp of REAL holds
( b₁ = diffreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 - r2 );