theorem :: JORDAN6:56

for P being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds
LE q,q,P