let p, q1, q2 be Point of (TOP-REAL 2); ( p in LSeg (q1,q2) implies (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )
assume
p in LSeg (q1,q2)
; (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)
; verum