theorem :: JGRAPH_6:74

for p1, p2, p3 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p3 in P & not ( LE p1,p2,P & LE p2,p3,P ) & not ( LE p1,p3,P & LE p3,p2,P ) & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p2,p3,P & LE p3,p1,P ) & not ( LE p3,p1,P & LE p1,p2,P ) holds
( LE p3,p2,P & LE p2,p1,P ) by Th73;