theorem Th17: :: JORDAN9:17

for G being Go-board
for p being Point of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
( p in cell (G,i,j) iff ( (G * (i,j)) `1 <= p `1 & p `1 <= (G * ((i + 1),j)) `1 & (G * (i,j)) `2 <= p `2 & p `2 <= (G * (i,(j + 1))) `2 ) )