theorem Th33: :: SURREALN:33

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