theorem Th8: :: PELLS_EQ:8

for n being Nat
for a, b being Real
for F being FinSequence of REAL st n > 1 & len F = n + 1 & ( for k being Nat st k in dom F holds
( a < F . k & F . k <= b ) ) holds
ex i, j being Nat st
( i in dom F & j in dom F & i <> j & F . i <= F . j & (F . j) - (F . i) < (b - a) / n )