let i, j be 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 Th3;
hence cell (G,i,j) is compact by TOPREAL6:78; :: thesis: verum