theorem :: JORDAN17:26

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