theorem :: JORDAN1H:63

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for i1, j2 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds
[(i1 -' 1),j2] in Indices (Gauge (C,n))