for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for r being Real ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r )