let k be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: 2 <= len G and
A2: 2 <= width G and
A3: f is_sequence_on G and
A4: 1 <= k and
A5: k + 1 <= len f ; :: thesis:
A6: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A4, A5, TOPREAL1:def 5;
consider i1, j1, i2, j2 being Element of NAT such that
A7: [i1,j1] in Indices G and
A8: f /. k = G * i1,j1 and
A9: [i2,j2] in Indices G and
A10: f /. (k + 1) = G * i2,j2 and
A11: ( ( 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, A5, JORDAN8:6;
A12: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A7, MATRIX_1:39;
A13: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A9, MATRIX_1:39;

per cases by A11;

suppose A14: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

then A15: j1 < width G by A13, XREAL_1:147;

now

per cases by A12, XXREAL_0:1;

suppose i1 < len G ; :: thesis:

then A16: i1 + 1 <= len G by NAT_1:13;
take i1 = i1; :: thesis:
take j1 = j1; :: thesis:
LSeg f,k c= cell G,i1,j1 by A6, A8, A10, A12, A14, A15, GOBOARD5:20;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A14, A16; :: thesis:

end;

suppose A17: i1 = len G ; :: thesis:

take i1' = i1 -' 1; :: thesis:
take j1 = j1; :: thesis:
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= i1' ) by A1, A17, NAT_D:42, XREAL_0:def 2;
then A18: 1 <= i1' by XXREAL_0:2;
A19: i1' + 1 = i1 by A12, XREAL_1:237;
then i1' < len G by A12, NAT_1:13;
then LSeg f,k c= cell G,i1',j1 by A6, A8, A10, A12, A14, A15, A19, GOBOARD5:19;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A14, A18, A19; :: thesis:

end;

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

end;

suppose A20: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

then A21: i1 < len G by A13, XREAL_1:147;

now

per cases by A12, XXREAL_0:1;

suppose j1 < width G ; :: thesis:

then A22: j1 + 1 <= width G by NAT_1:13;
take i1 = i1; :: thesis:
take j1 = j1; :: thesis:
LSeg f,k c= cell G,i1,j1 by A6, A8, A10, A12, A20, A21, GOBOARD5:23;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A20, A22; :: thesis:

end;

suppose A23: j1 = width G ; :: thesis:

take i1 = i1; :: thesis:
take j1' = j1 -' 1; :: thesis:
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= j1' ) by A2, A23, NAT_D:42, XREAL_0:def 2;
then A24: 1 <= j1' by XXREAL_0:2;
A25: j1' + 1 = j1 by A12, XREAL_1:237;
then j1' < width G by A23, NAT_1:13;
then LSeg f,k c= cell G,i1,j1' by A6, A8, A10, A12, A20, A21, A25, GOBOARD5:22;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A20, A24, A25; :: thesis:

end;

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

end;

suppose A26: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

then A27: i2 < len G by A12, XREAL_1:147;

now

per cases by A12, XXREAL_0:1;

suppose j1 < width G ; :: thesis:

then A28: j1 + 1 <= width G by NAT_1:13;
take i2 = i2; :: thesis:
take j1 = j1; :: thesis:
LSeg f,k c= cell G,i2,j1 by A6, A8, A10, A13, A26, A27, GOBOARD5:23;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A26, A28; :: thesis:

end;

suppose A29: j1 = width G ; :: thesis:

take i2 = i2; :: thesis:
take j1' = j1 -' 1; :: thesis:
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= j1' ) by A2, A29, NAT_D:42, XREAL_0:def 2;
then A30: 1 <= j1' by XXREAL_0:2;
A31: j1' + 1 = j1 by A12, XREAL_1:237;
then j1' < width G by A29, NAT_1:13;
then LSeg f,k c= cell G,i2,j1' by A6, A8, A10, A13, A26, A27, A31, GOBOARD5:22;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A26, A30, A31; :: thesis:

end;

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

end;

suppose A32: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

then A33: j2 < width G by A12, XREAL_1:147;

now

per cases by A12, XXREAL_0:1;

suppose i1 < len G ; :: thesis:

then A34: i1 + 1 <= len G by NAT_1:13;
take i1 = i1; :: thesis:
take j2 = j2; :: thesis:
LSeg f,k c= cell G,i1,j2 by A6, A8, A10, A13, A32, A33, GOBOARD5:20;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A32, A34; :: thesis:

end;

suppose A35: i1 = len G ; :: thesis:

take i1' = i1 -' 1; :: thesis:
take j2 = j2; :: thesis:
( 2 - 1 <= 2 -' 1 & 2 -' 1 <= i1' ) by A1, A35, NAT_D:42, XREAL_0:def 2;
then A36: 1 <= i1' by XXREAL_0:2;
A37: i1' + 1 = i1 by A12, XREAL_1:237;
then i1' < len G by A12, NAT_1:13;
then LSeg f,k c= cell G,i1',j2 by A6, A8, A10, A13, A32, A33, A37, GOBOARD5:19;
hence ex i, j being Element of NAT st
( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & LSeg f,k c= cell G,i,j ) by A12, A13, A32, A36, A37; :: thesis:

end;

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

end;