theorem :: SURREALR:66

for x1, x2, y1, y2 being Surreal st x1 == x2 & y1 == y2 holds
x1 + y1 == x2 + y2 by Th43;