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

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