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