theorem Th54: :: SURREALN:54

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