let n be Nat; :: thesis: 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); :: thesis: 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; :: thesis: verum