theorem Th10: :: JORDAN5B:10

for p, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg (p1,p2) holds
LE p1,p,p1,p2