theorem Th11: :: GOBOARD2:11

for f being FinSequence of (TOP-REAL 2)
for G being Go-board st f is special holds
for n being Nat st n in dom f & n + 1 in dom f holds
for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j