for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )