theorem Th2: :: SURREALN:2
for x being Surreal
for n being Nat st x in Day n holds
( uInt . (- n) <= x & x <= uInt . n )