theorem Th31: :: JGRAPH_1:31

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