:: deftheorem defines + SURREALR:def 7 :
for x, y being Surreal holds x + y = (No_sum_op ((born x) (+) (born y))) . [x,y];