:: deftheorem Def11 defines +' SURREALR:def 11 :
for x, y being object st x is surreal & y is surreal holds
for b₃ being Surreal holds
( b₃ = x +' y iff for x1, y1 being Surreal st x1 = x & y1 = y holds
b₃ = x1 + y1 );