theorem :: EUCLID_8:73

for p1, p2 being Element of REAL 3 holds |((- p1),(- p2))| = |(p1,p2)| by RVSUM_1:133;