theorem :: JORDAN1F:13

for i being Nat
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )