theorem Th26: :: JORDAN1B:26

for n being Nat
for C being Simple_closed_curve
for i being Nat st 1 < i & i < len (Gauge (C,n)) holds
LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Lower_Arc C