theorem Th10: :: GOBOARD7:10

for f being non empty FinSequence of (TOP-REAL 2)
for k being Nat st LSeg (f,k) is horizontal holds
ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )