theorem :: EUCLID_2:49

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