theorem :: JORDAN16:7

for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C