theorem :: JGRAPH_3:1

for p being Point of (TOP-REAL 2) holds
( |.p.| = sqrt (((p `1) ^2) + ((p `2) ^2)) & |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) ) by JGRAPH_1:29, JGRAPH_1:30;