theorem :: JORDAN15:16

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 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )