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 horizontal holds
ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )