let i, j be 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 Th18, Th19;

hence cell (G,i,j) is convex by GOBOARD9:6; :: thesis: verum

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 Th18, Th19;

hence cell (G,i,j) is convex by GOBOARD9:6; :: thesis: verum