theorem Th21: :: TOPREAL1:21

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