let n be Nat; for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r))
let p, q, r be Point of (TOP-REAL n); dist (p,r) <= (dist (p,q)) + (dist (q,r))
A1:
ex a, b being Point of (Euclid n) st
( a = p & b = r & dist (a,b) = dist (p,r) )
by Def1;
A2:
ex a, b being Point of (Euclid n) st
( a = q & b = r & dist (a,b) = dist (q,r) )
by Def1;
ex a, b being Point of (Euclid n) st
( a = p & b = q & dist (a,b) = dist (p,q) )
by Def1;
hence
dist (p,r) <= (dist (p,q)) + (dist (q,r))
by A1, A2, METRIC_1:4; verum