theorem Th21: :: JORDAN9:21

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