theorem Th44: :: EUCLID_2:46

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