theorem Th34: :: EUCLID_2:36

for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| = |.p.| ^2 by Th4;