let k be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f holds
( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f holds
( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f implies ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) )
assume that
A1: f is_sequence_on G and
A2: f is special and
A3: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
consider i1, j1, i2, j2 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * i1,j1 and
A6: [i2,j2] in Indices G and
A7: f /. (k + 1) = G * i2,j2 and
A8: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A3, JORDAN8:6;
A9: i2 <= len G by A6, MATRIX_1:39;
A10: i1 <= len G by A4, MATRIX_1:39;
then A11: i1 -' 1 <= len G by NAT_D:44;
A12: j2 <= width G by A6, MATRIX_1:39;
then A13: j2 -' 1 <= width G by NAT_D:44;
A14: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A15: j1 <= width G by A4, MATRIX_1:39;
then A16: j1 -' 1 <= width G by NAT_D:44;
A17: ( i1 + 1 > i1 & i2 + 1 > i2 ) by NAT_1:13;

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 A8;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )

then ( right_cell f,k,G = cell G,i1,j1 & left_cell f,k,G = cell G,(i1 -' 1),j1 ) by A1, A3, A4, A5, A6, A7, A14, GOBRD13:def 2, GOBRD13:def 3;
hence ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) by A1, A2, A10, A15, A11, Th16; :: thesis: verum

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )

then ( right_cell f,k,G = cell G,i1,(j1 -' 1) & left_cell f,k,G = cell G,i1,j1 ) by A1, A3, A4, A5, A6, A7, A17, GOBRD13:def 2, GOBRD13:def 3;
hence ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) by A1, A2, A10, A15, A16, Th16; :: thesis: verum

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )

then ( right_cell f,k,G = cell G,i2,j2 & left_cell f,k,G = cell G,i2,(j2 -' 1) ) by A1, A3, A4, A5, A6, A7, A17, GOBRD13:def 2, GOBRD13:def 3;
hence ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) by A1, A2, A9, A12, A13, Th16; :: thesis: verum

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )

then ( right_cell f,k,G = cell G,(i1 -' 1),j2 & left_cell f,k,G = cell G,i1,j2 ) by A1, A3, A4, A5, A6, A7, A14, GOBRD13:def 2, GOBRD13:def 3;
hence ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) by A1, A2, A10, A12, A11, Th16; :: thesis: verum

end;

end;