theorem Th17: :: EUCLID_6:17

for p1, p2, p3, p being Point of (TOP-REAL 2) st p in LSeg (p1,p2) & p <> p2 holds
( |((p3 - p),(p2 - p1))| = 0 iff |((p3 - p),(p2 - p))| = 0 )