theorem Th3: :: JORDAN12:3

for n being Nat
for f being FinSequence of (TOP-REAL n)
for i being Nat st 1 <= i & i + 1 <= len f holds
( f /. i in rng f & f /. (i + 1) in rng f )