let q1, q2, p 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:31; :: thesis: verum