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