:: deftheorem Def1 defines Euclid_add REAL_NS1:def 1 :
for n being Nat
for b₂ being BinOp of (REAL n) holds
( b₂ = Euclid_add n iff for a, b being Element of REAL n holds b₂ . (a,b) = a + b );