for X being RealNormSpace
for x being Element of REAL
for v being Point of RNS_Real st x = v holds
- x = - v