let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) )
assume A1: f is_sequence_on G ; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )
then consider i1, j1, i2, j2 being Nat such that
A3: [i1,j1] in Indices G and
A4: f /. k = G * (i1,j1) and
A5: [i2,j2] in Indices G and
A6: f /. (k + 1) = G * (i2,j2) and
A7: ( ( 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, JORDAN8:3;
A8: i2 <= len G by A5, MATRIX_0:32;
A9: i1 <= len G by A3, MATRIX_0:32;
then A10: i1 -' 1 <= len G by NAT_D:44;
A11: j2 <= width G by A5, MATRIX_0:32;
then A12: j2 -' 1 <= width G by NAT_D:44;
A13: ( j1 + 1 > j1 & j2 + 1 > j2 ) by NAT_1:13;
A14: j1 <= width G by A3, MATRIX_0:32;
then A15: j1 -' 1 <= width G by NAT_D:44;
A16: ( 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 A7;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )

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, A13, GOBRD13:def 2, GOBRD13:def 3, A2;
hence ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) by A9, A14, A10, GOBOARD9:14; :: thesis: verum

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )

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, A16, GOBRD13:def 2, GOBRD13:def 3, A2;
hence ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) by A9, A14, A15, GOBOARD9:14; :: thesis: verum

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )

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, A16, GOBRD13:def 2, GOBRD13:def 3, A2;
hence ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) by A8, A11, A12, GOBOARD9:14; :: thesis: verum

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} )

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, A13, GOBRD13:def 2, GOBRD13:def 3, A2;
hence ( Int (left_cell (f,k,G)) <> {} & Int (right_cell (f,k,G)) <> {} ) by A9, A11, A10, GOBOARD9:14; :: thesis: verum

end;

end;