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 ) )