theorem Th13: :: JORDAN15:13

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )