theorem Th31: :: BHSP_1:31

for X being RealUnitarySpace
for x being Point of X holds ||.(- x).|| = ||.x.||