theorem Th11: :: GOBOARD7:11

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