theorem :: EUCLID_8:81

for p, q being Element of REAL 3 holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:139;