theorem Th45: :: SURREALN:45

for i1, i2 being Integer
for n1, n2 being Nat st i1 / (2 |^ n1) < i2 / (2 |^ n2) holds
( i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) & (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) )