theorem Th4: :: SURREALN:4

for n being Nat holds
( n = born (uInt . n) & n = born (uInt . (- n)) )