theorem Th25: :: JORDAN1B:25

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 Upper_Arc C