theorem Th24: :: JORDAN5C:24

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