let i, j be Element of NAT ; :: thesis: for G being Go-board st i <= len G & j <= width G holds
Int (cell G,i,j) <> {}
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies Int (cell G,i,j) <> {} )
assume that
A1: i <= len G and
A2: j <= width G ; :: thesis: Int (cell G,i,j) <> {}
A3: ( j = width G or j < width G ) by A2, XXREAL_0:1;
A4: ( i = len G or i < len G ) by A1, XXREAL_0:1;
consider p being Point of (TOP-REAL 2);

per cases ( ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) or ( 1 <= i & i + 1 <= len G & j = width G ) or ( 1 <= i & i + 1 <= len G & j = 0 ) or ( 1 <= j & j + 1 <= width G & i = 0 ) or ( 1 <= j & j + 1 <= width G & i = len G ) or ( i = 0 & j = 0 ) or ( i = len G & j = width G ) or ( i = 0 & j = width G ) or ( i = len G & j = 0 ) ) by A3, A4, NAT_1:13, NAT_1:14;

suppose ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),p meets Int (cell G,i,j) by GOBOARD6:85;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( 1 <= i & i + 1 <= len G & j = width G ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,(((1 / 2) * ((G * i,j) + (G * (i + 1),j))) + |[0 ,1]|) meets Int (cell G,i,j) by GOBOARD6:86;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( 1 <= i & i + 1 <= len G & j = 0 ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg (((1 / 2) * ((G * i,(j + 1)) + (G * (i + 1),(j + 1)))) - |[0 ,1]|),p meets Int (cell G,i,j) by GOBOARD6:87;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( 1 <= j & j + 1 <= width G & i = 0 ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg (((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) - |[1,0 ]|),p meets Int (cell G,i,j) by GOBOARD6:88;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( 1 <= j & j + 1 <= width G & i = len G ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,(((1 / 2) * ((G * i,j) + (G * i,(j + 1)))) + |[1,0 ]|) meets Int (cell G,i,j) by GOBOARD6:89;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( i = 0 & j = 0 ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,((G * (i + 1),(j + 1)) - |[1,1]|) meets Int (cell G,i,j) by GOBOARD6:90;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( i = len G & j = width G ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,((G * i,j) + |[1,1]|) meets Int (cell G,i,j) by GOBOARD6:91;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( i = 0 & j = width G ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,((G * (i + 1),j) + |[(- 1),1]|) meets Int (cell G,i,j) by GOBOARD6:92;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

suppose ( i = len G & j = 0 ) ; :: thesis: Int (cell G,i,j) <> {}

then LSeg p,((G * i,(j + 1)) + |[1,(- 1)]|) meets Int (cell G,i,j) by GOBOARD6:93;
hence Int (cell G,i,j) <> {} by XBOOLE_1:65; :: thesis: verum

end;

end;