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;