theorem Th7: :: SURREALN:7
for n being Nat holds
( L_ (uInt . (- n)) = {} & {} = R_ (uInt . n) )