let n be Element of 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