theorem Th12: :: GOBOARD5:12

for f being non empty standard FinSequence of (TOP-REAL 2)
for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices (GoB f) & [i,j] in Indices (GoB f) & f /. n = (GoB f) * (m,k) & f /. (n + 1) = (GoB f) * (i,j) holds
|.(m - i).| + |.(k - j).| = 1