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