theorem Th28: :: EUCLID_2:30

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)|