theorem Th8: :: JORDAN17:8
for P being Simple_closed_curve
for a, b being Point of (TOP-REAL 2) st a <> b & LE a,b,P holds
ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )