theorem Th29: :: EUCLID_2:31

for n being Nat
for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|