theorem Th21: :: JORDAN1B:21

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