theorem :: JORDAN1B:22

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