theorem
for
G being
Go-board for
f being
FinSequence of
(TOP-REAL 2) st 1
<= len f &
f /. 1
in rng (Line (G,1)) &
f /. (len f) in rng (Line (G,(len G))) &
f is_sequence_on G holds
( ( for
i being
Nat st 1
<= i &
i <= len G holds
ex
k being
Nat st
(
k in dom f &
f /. k in rng (Line (G,i)) ) ) & ( for
i being
Nat st 1
<= i &
i <= len G & 2
<= len f holds
L~ f meets rng (Line (G,i)) ) & ( for
i,
j,
k,
m being
Nat st 1
<= i &
i <= len G & 1
<= j &
j <= len G &
k in dom f &
m in dom f &
f /. k in rng (Line (G,i)) & ( for
n being
Nat st
n in dom f &
f /. n in rng (Line (G,i)) holds
n <= k ) &
k < m &
f /. m in rng (Line (G,j)) holds
i < j ) )