theorem Th59: :: SURREALN:59
for x being Surreal
for n being positive Nat holds
( x - ((uInt . n) ") < real_qua x & real_qua x < x + ((uInt . n) ") )