theorem Th44: :: SURREALN:44

for n being Nat
for r being Real holds
( uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . r & sReal . r < uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )