theorem :: EUCLID_8:74

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