let i, j be Element of NAT ; :: thesis: for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
cell G,i,j is compact
let G be Go-board; :: thesis: ( 1 <= i & i < len G & 1 <= j & j < width G implies cell G,i,j is compact )
assume ( 1 <= i & i < len G & 1 <= j & j < width G ) ; :: thesis: cell G,i,j is compact
then cell G,i,j = product (1,2 --> [.((G * i,1) `1 ),((G * (i + 1),1) `1 ).],[.((G * 1,j) `2 ),((G * 1,(j + 1)) `2 ).]) by Th13;
hence cell G,i,j is compact by TOPREAL6:87; :: thesis: verum