theorem Th29: :: JGRAPH_1:29

for p being Point of (TOP-REAL 2) holds |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2)