theorem :: JORDAN1J:62

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Upper_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Lower_Arc (L~ (Cage (C,(n + 1))))