theorem :: JGRAPH_6:76

for p1, p2, p3, p4 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 & p4 in P & LE p2,p3,P & LE p3,p4,P & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p3,p1,P & LE p1,p4,P ) holds
LE p4,p1,P by Th73;