theorem Th13: :: JORDAN9:13

for k being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & LSeg (f,k) is vertical holds
ex i being Nat st
( 1 <= i & i <= len G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `1 = (G * (i,1)) `1 ) )