for n being Nat
for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r))