theorem :: EUCLID_2:22

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |(p1,(- p2))| = - |(p1,p2)| by Th19;