:: deftheorem defines diffrat BINOP_2:def 16 :
for b₁ being BinOp of RAT holds
( b₁ = diffrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 - w2 );