:: deftheorem Def9 defines addreal BINOP_2:def 9 :
for b₁ being BinOp of REAL holds
( b₁ = addreal iff for r1, r2 being Real holds b₁ . (r1,r2) = r1 + r2 );