let p, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (q1,q2) implies (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )
assume p in LSeg (q1,q2) ; :: thesis: (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2)
then consider r being Real such that
A1: ( p = ((1 - r) * q1) + (r * q2) & 0 <= r & r <= 1 ) ;
( dist (q1,p) = r * (dist (q1,q2)) & dist (q2,p) = (1 - r) * (dist (q1,q2)) ) by A1, Th27, Th28;
hence (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ; :: thesis: verum