theorem :: JORDAN17:25
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b are_in_this_order_on P holds
b = d