theorem Th10: :: EUCLID12:12

for p, q1, q2 being Point of (TOP-REAL 2) holds
( p in LSeg (q1,q2) iff (dist (q1,p)) + (dist (p,q2)) = dist (q1,q2) )