theorem Th20: :: JORDAN9:20

for i, j being Nat
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
( G * (i,j) in cell (G,i,j) & G * (i,(j + 1)) in cell (G,i,j) & G * ((i + 1),(j + 1)) in cell (G,i,j) & G * ((i + 1),j) in cell (G,i,j) )