let p, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( q1 in LSeg (q2,p) & q1 <> q2 implies dist (q1,p) < dist (q2,p) )
assume that
A1: q1 in LSeg (q2,p) and
A2: q1 <> q2 ; :: thesis: dist (q1,p) < dist (q2,p)
(dist (q2,q1)) + (dist (q1,p)) = dist (q2,p) by A1, Th29;
hence dist (q1,p) < dist (q2,p) by A2, Th22, XREAL_1:29; :: thesis: verum