theorem Th5: :: SURREALN:5

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