theorem Th7: :: JORDAN9:7

for n being Nat
for f being FinSequence of (TOP-REAL 2)
for x being set st n <= len f & x in L~ (f /^ n) holds
ex i being Nat st
( n + 1 <= i & i + 1 <= len f & x in LSeg (f,i) )