let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 2),j1] in Indices (Gauge C,n)
let n be Element of NAT ; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 2),j1] in Indices (Gauge C,n)
set G = Gauge C,n;
A1: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on Gauge C,n & len f > 1 implies for i1, j1 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 2),j1] in Indices (Gauge C,n) )
assume that
A2: f is_sequence_on Gauge C,n and
A3: len f > 1 ; :: thesis: for i1, j1 being Element of NAT st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 2),j1] in Indices (Gauge C,n)
A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:237;
let i1, j1 be Element of NAT ; :: thesis: ( front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 implies [(i1 + 2),j1] in Indices (Gauge C,n) )
assume that
A5: ( front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 ) and
A6: [(i1 + 1),j1] in Indices (Gauge C,n) and
A7: f /. (len f) = (Gauge C,n) * (i1 + 1),j1 ; :: thesis: [(i1 + 2),j1] in Indices (Gauge C,n)
A8: j1 <= width (Gauge C,n) by A6, MATRIX_1:39;
A9: i1 + 1 <= len (Gauge C,n) by A6, MATRIX_1:39;

A10: now

assume (i1 + 1) + 1 > len (Gauge C,n) ; :: thesis: contradiction
then A11: (len (Gauge C,n)) + 1 <= (i1 + 1) + 1 by NAT_1:13;
(i1 + 1) + 1 <= (len (Gauge C,n)) + 1 by A9, XREAL_1:8;
then (i1 + 1) + 1 = (len (Gauge C,n)) + 1 by A11, XXREAL_0:1;
then cell (Gauge C,n),(len (Gauge C,n)),j1 meets C by A2, A5, A6, A7, A4, GOBRD13:37;
hence contradiction by A1, A8, JORDAN8:19; :: thesis: verum

end;

A12: 1 <= (i1 + 1) + 1 by NAT_1:12;
1 <= j1 by A6, MATRIX_1:39;
hence [(i1 + 2),j1] in Indices (Gauge C,n) by A8, A12, A10, MATRIX_1:37; :: thesis: verum