let i, j be Nat; :: thesis: for G being Go-board st i <= len G & j <= width G holds
not cell (G,i,j) is empty
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies not cell (G,i,j) is empty )
assume ( i <= len G & j <= width G ) ; :: thesis: not cell (G,i,j) is empty
then not Int (cell (G,i,j)) is empty by GOBOARD9:14;
hence not cell (G,i,j) is empty by TOPS_1:16, XBOOLE_1:3; :: thesis: verum