let i, j be Element of NAT ; :: thesis: for G being Go-board st i <= len G & j <= width G holds
cell G,i,j is connected
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies cell G,i,j is connected )
assume A1: ( i <= len G & j <= width G ) ; :: thesis: cell G,i,j is connected
Cl (Int (cell G,i,j)) is connected by A1, CONNSP_1:20, GOBOARD9:21;
hence cell G,i,j is connected by A1, GOBRD11:35; :: thesis: verum