theorem :: ANPROJ10:26

for x being Element of (TOP-REAL 1)
for p being Tuple of 1, REAL st p = x holds
- x = - p ;