theorem :: EUCLID:71

for n being Nat
for p being Point of (TOP-REAL n) holds |.(- p).| = |.p.| by Th7;