theorem Th32: :: JGRAPH_1:32

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