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