for N being Nat
for w, w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|