let p, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (q1,q2) iff (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )
thus ( p in LSeg (q1,q2) implies (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ) by JORDAN1K:29; :: thesis: ( (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) implies p in LSeg (q1,q2) )
assume A1: (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) ; :: thesis: p in LSeg (q1,q2)
reconsider w1 = q1, w2 = p, w3 = q2 as Element of REAL 2 by EUCLID:22;
reconsider z1 = q1, z2 = p, z3 = q2 as Point of (Euclid 2) by EUCLID:67;
A2: ( dist (z1,z2) = |.(w1 - w2).| & dist (z1,z3) = |.(w1 - w3).| & dist (z2,z3) = |.(w2 - w3).| ) by SPPOL_1:5;
( dist (z1,z2) = dist (q1,p) & dist (z1,z3) = dist (q1,q2) & dist (z2,z3) = dist (p,q2) ) by TOPREAL6:def 1;
then |.(q1 - p).| + |.(p - q2).| = |.(q1 - q2).| by A1, A2;
hence p in LSeg (q1,q2) by Th9; :: thesis: verum