theorem Th13: :: JORDAN19:13

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 <= k & k <= j & j <= width (Gauge (C,n)) & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} & (LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) meets Lower_Arc C