theorem Th28: :: SURREALR:28

for x, y being Surreal holds x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))]