theorem Th23: :: JORDAN15:23

for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (i,k) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (i,j) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C