theorem :: EUCLID_8:72

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