theorem Th2: :: NORMSP_1:2

for RNS being RealNormSpace
for x being Point of RNS holds ||.(- x).|| = ||.x.||