let i, j be Nat; :: thesis: for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) is convex
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) is convex )
assume that
A1: i <= len G and
A2: j <= width G ; :: thesis: Int (cell (G,i,j)) is convex
set P = Int (cell (G,i,j));
A3: Int (cell (G,i,j)) = (Int (v_strip (G,i))) /\ (Int (h_strip (G,j))) by TOPS_1:17;
A4: Int (v_strip (G,i)) is convex by A1, Th12;
Int (h_strip (G,j)) is convex by A2, Th11;
hence Int (cell (G,i,j)) is convex by A3, A4, Th5; :: thesis: verum