let i, j be 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;
set p = the 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))))), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:82;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( 1 <= i & i + 1 <= len G & j = width G ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * ((i + 1),j)))) + |[0,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:83;
hence Int (cell (G,i,j)) <> {} ; :: 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]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:84;
hence Int (cell (G,i,j)) <> {} ; :: 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]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:85;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( 1 <= j & j + 1 <= width G & i = len G ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1))))) + |[1,0]|)) meets Int (cell (G,i,j)) by GOBOARD6:86;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( i = 0 & j = 0 ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),(j + 1))) - |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:87;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( i = len G & j = width G ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),((G * (i,j)) + |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:88;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( i = 0 & j = width G ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),j)) + |[(- 1),1]|)) meets Int (cell (G,i,j)) by GOBOARD6:89;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
suppose ( i = len G & j = 0 ) ; :: thesis: Int (cell (G,i,j)) <> {}
then LSeg ( the Point of (TOP-REAL 2),((G * (i,(j + 1))) + |[1,(- 1)]|)) meets Int (cell (G,i,j)) by GOBOARD6:90;
hence Int (cell (G,i,j)) <> {} ; :: thesis: verum
end;
end;