theorem Th53: :: SURREALN:53

for r1, r2 being Real st r1 < r2 holds
ex n being Nat st [\((r1 * (2 |^ n)) + 1)/] / (2 |^ n) < r2