:: deftheorem Def15 defines addrat BINOP_2:def 15 :
for b₁ being BinOp of RAT holds
( b₁ = addrat iff for w1, w2 being Rational holds b₁ . (w1,w2) = w1 + w2 );