theorem :: JORDAN1J:63

for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Upper_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))} & (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) /\ (Lower_Arc (L~ (Cage (C,(n + 1))))) = {((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))} holds
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k))) meets Lower_Arc C