theorem Th32: :: SURREALN:32

for x1, x2, y1, y2, p1, p2 being Nat st x1 + (y1 / (2 |^ p1)) = x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 holds
x1 = x2