theorem Th7: :: SURREALR:7

for x being Surreal holds - x = [(-- (R_ x)),(-- (L_ x))]