theorem :: JORDAN17:10

for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds
b,c,d,a are_in_this_order_on P ;