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 convex
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies cell G,i,j is convex )
assume ( i <= len G & j <= width G ) ; :: thesis: cell G,i,j is convex
then ( v_strip G,i is convex & h_strip G,j is convex ) by Th19, Th20;
hence cell G,i,j is convex by GOBOARD9:9; :: thesis: verum