theorem Th17: :: ANPROJ10:30

for T being RealLinearSpace
for x being Element of T
for p being Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x holds
- p = - x