let i, j be Element of 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:17;
hence not cell G,i,j is empty by TOPS_1:44, XBOOLE_1:3; :: thesis: verum