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