theorem :: JORDAN7:20

for P being non empty compact Subset of (TOP-REAL 2)
for e being Real st P is being_simple_closed_curve & e > 0 holds
ex h being FinSequence of the carrier of (TOP-REAL 2) st
( h . 1 = W-min P & h is one-to-one & 8 <= len h & rng h c= P & ( for i being Nat st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),P ) & ( for i being Nat
for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),P) holds
diameter W < e ) & ( for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),P) holds
diameter W < e ) & ( for i being Nat st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),P)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),P)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),P)) /\ (Segment ((h /. 1),(h /. 2),P)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),P)) /\ (Segment ((h /. (len h)),(h /. 1),P)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),P) misses Segment ((h /. 1),(h /. 2),P) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds
Segment ((h /. i),(h /. (i + 1)),P) misses Segment ((h /. j),(h /. (j + 1)),P) ) & ( for i being Nat st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),P) misses Segment ((h /. i),(h /. (i + 1)),P) ) )