theorem Th17: :: SURREALN:17

for x, y being Surreal st x = [{y},{}] & born x is finite & 0_No <= y holds
ex n being Nat st
( x == uInt . (n + 1) & uInt . n <= y & y < uInt . (n + 1) & n in born x )