let i, j be Nat; 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; ( 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
; 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; verum