theorem :: JORDAN17:9

for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st a in P holds
a,a,a,a are_in_this_order_on P by JORDAN6:56;