theorem Th57: :: SURREALC:57

for x, y being Surreal
for n being positive Nat st |.y.| * (uReal . ((n + 1) / n)) < |.x.| holds
|.x.|,|.(x + y).| are_commensurate