theorem Th9: :: REAL_NS2:9

for n being Nat
for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
- q = - g