for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st a in P holds
ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P )