theorem Th20: :: GOBOARD1:27

for n, i being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds
for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds
|.(n - k).| = 1