let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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 j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds
for j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
set G = Gauge (C,n);
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A1: f is_sequence_on Gauge (C,n) and
A2: len f > 1 ; :: thesis: for j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds
[i2,(j1 -' 1)] in Indices (Gauge (C,n))
A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235;
let j1, i2 be Nat; :: thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [i2,(j1 -' 1)] in Indices (Gauge (C,n)) )
assume that
A4: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and
A5: [i2,j1] in Indices (Gauge (C,n)) and
A6: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; :: thesis: [i2,(j1 -' 1)] in Indices (Gauge (C,n))
A7: i2 <= len (Gauge (C,n)) by A5, MATRIX_0:32;
A8: 1 <= j1 by A5, MATRIX_0:32;

A9: now :: thesis: not j1 -' 1 < 1

assume j1 -' 1 < 1 ; :: thesis: contradiction
then j1 <= 1 by NAT_1:14, NAT_D:36;
then j1 = 1 by A8, XXREAL_0:1;
then cell ((Gauge (C,n)),i2,(1 -' 1)) meets C by A1, A4, A5, A6, A3, GOBRD13:25;
then cell ((Gauge (C,n)),i2,0) meets C by XREAL_1:232;
hence contradiction by A7, JORDAN8:17; :: thesis: verum

end;

A10: j1 -' 1 <= j1 by NAT_D:35;
j1 <= width (Gauge (C,n)) by A5, MATRIX_0:32;
then A11: j1 -' 1 <= width (Gauge (C,n)) by A10, XXREAL_0:2;
1 <= i2 by A5, MATRIX_0:32;
hence [i2,(j1 -' 1)] in Indices (Gauge (C,n)) by A7, A11, A9, MATRIX_0:30; :: thesis: verum