theorem :: JORDAN18:33

for C being Simple_closed_curve
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds
p1,q1 are_neighbours_wrt p2,q2,C