theorem :: GOBOARD1:37

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