let k be Nat; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f holds
ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f holds
ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f implies ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) )
assume that
A1: 2 <= len G and
A2: 2 <= width G and
A3: f is_sequence_on G and
A4: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
consider i1, j1, i2, j2 being Nat such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) and
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) and
A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A3, A4, JORDAN8:3;
A10: LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) by A4, TOPREAL1:def 3;
A11: 1 <= i2 by A7, MATRIX_0:32;
A12: 1 <= i1 by A5, MATRIX_0:32;
A13: 1 <= j2 by A7, MATRIX_0:32;
A14: 1 <= j1 by A5, MATRIX_0:32;
A15: i2 <= len G by A7, MATRIX_0:32;
A16: i1 <= len G by A5, MATRIX_0:32;
A17: j2 <= width G by A7, MATRIX_0:32;
A18: j1 <= width G by A5, MATRIX_0:32;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9;

suppose A19: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

then A20: j1 < width G by A17, XREAL_1:145;

now :: thesis: ex i1, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

per cases ( i1 < len G or i1 = len G ) by A16, XXREAL_0:1;

suppose A21: i1 < len G ; :: thesis: ex i1, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

take i1 = i1; :: thesis: ex j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j1 = j1; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
A22: i1 + 1 <= len G by A21, NAT_1:13;
LSeg (f,k) c= cell (G,i1,j1) by A10, A6, A8, A12, A16, A14, A17, A19, GOBOARD5:19, XREAL_1:145;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A12, A14, A17, A19, A22; :: thesis: verum

end;

suppose A23: i1 = len G ; :: thesis: ex i19, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

reconsider i19 = i1 -' 1, j1 = j1 as Nat ;
take i19 = i19; :: thesis: ex j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j1 = j1; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= i19 ) by A1, A23, NAT_D:42, XREAL_0:def 2;
then A24: 1 <= i19 by XXREAL_0:2;
A25: i19 + 1 = i1 by A12, XREAL_1:235;
then i19 < len G by A16, NAT_1:13;
then LSeg (f,k) c= cell (G,i19,j1) by A10, A6, A8, A14, A19, A20, A25, GOBOARD5:18;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A16, A14, A17, A19, A24, A25; :: thesis: verum

end;

end;

end;

hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) ; :: thesis: verum

end;

suppose A26: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

then A27: i1 < len G by A15, XREAL_1:145;

now :: thesis: ex i1, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

per cases ( j1 < width G or j1 = width G ) by A18, XXREAL_0:1;

suppose A28: j1 < width G ; :: thesis: ex i1, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

take i1 = i1; :: thesis: ex j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j1 = j1; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
A29: j1 + 1 <= width G by A28, NAT_1:13;
LSeg (f,k) c= cell (G,i1,j1) by A10, A6, A8, A12, A14, A18, A15, A26, GOBOARD5:22, XREAL_1:145;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A12, A14, A15, A26, A29; :: thesis: verum

end;

suppose A30: j1 = width G ; :: thesis: ex i1, j19, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

reconsider i1 = i1, j19 = j1 -' 1 as Nat ;
take i1 = i1; :: thesis: ex j19, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j19 = j19; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= j19 ) by A2, A30, NAT_D:42, XREAL_0:def 2;
then A31: 1 <= j19 by XXREAL_0:2;
A32: j19 + 1 = j1 by A14, XREAL_1:235;
then j19 < width G by A30, NAT_1:13;
then LSeg (f,k) c= cell (G,i1,j19) by A10, A6, A8, A12, A26, A27, A32, GOBOARD5:21;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A12, A18, A15, A26, A31, A32; :: thesis: verum

end;

end;

end;

hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) ; :: thesis: verum

end;

suppose A33: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

then A34: i2 < len G by A16, XREAL_1:145;

now :: thesis: ex i2, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

per cases ( j1 < width G or j1 = width G ) by A18, XXREAL_0:1;

suppose A35: j1 < width G ; :: thesis: ex i2, j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

take i2 = i2; :: thesis: ex j1, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j1 = j1; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
A36: j1 + 1 <= width G by A35, NAT_1:13;
LSeg (f,k) c= cell (G,i2,j1) by A10, A6, A8, A16, A11, A13, A17, A33, GOBOARD5:22, XREAL_1:145;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A16, A14, A11, A33, A36; :: thesis: verum

end;

suppose A37: j1 = width G ; :: thesis: ex i2, j19, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

reconsider i2 = i2, j19 = j1 -' 1 as Nat ;
take i2 = i2; :: thesis: ex j19, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j19 = j19; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= j19 ) by A2, A37, NAT_D:42, XREAL_0:def 2;
then A38: 1 <= j19 by XXREAL_0:2;
A39: j19 + 1 = j1 by A14, XREAL_1:235;
then j19 < width G by A37, NAT_1:13;
then LSeg (f,k) c= cell (G,i2,j19) by A10, A6, A8, A11, A33, A34, A39, GOBOARD5:21;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A16, A18, A11, A33, A38, A39; :: thesis: verum

end;

end;

end;

hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) ; :: thesis: verum

end;

suppose A40: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

then A41: j2 < width G by A18, XREAL_1:145;

now :: thesis: ex i1, j2, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

per cases ( i1 < len G or i1 = len G ) by A16, XXREAL_0:1;

suppose A42: i1 < len G ; :: thesis: ex i1, j2, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

take i1 = i1; :: thesis: ex j2, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j2 = j2; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
A43: i1 + 1 <= len G by A42, NAT_1:13;
LSeg (f,k) c= cell (G,i1,j2) by A10, A6, A8, A18, A11, A15, A13, A40, GOBOARD5:19, XREAL_1:145;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A12, A18, A13, A40, A43; :: thesis: verum

end;

suppose A44: i1 = len G ; :: thesis: ex i19, j2, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )

reconsider i19 = i1 -' 1, j2 = j2 as Nat ;
take i19 = i19; :: thesis: ex j2, i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
take j2 = j2; :: thesis: ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) )
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= i19 ) by A1, A44, NAT_D:42, XREAL_0:def 2;
then A45: 1 <= i19 by XXREAL_0:2;
A46: i19 + 1 = i1 by A12, XREAL_1:235;
then i19 < len G by A16, NAT_1:13;
then LSeg (f,k) c= cell (G,i19,j2) by A10, A6, A8, A13, A40, A41, A46, GOBOARD5:18;
hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) by A16, A18, A13, A40, A45, A46; :: thesis: verum

end;

end;

end;

hence ex i, j being Nat st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg (f,k) c= cell (G,i,j) ) ; :: thesis: verum

end;

end;