theorem Th23: :: JORDAN5C:23

for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is being_S-Seq & 1 <= i & i + 1 <= len f holds
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)