theorem :: SPRECT_3:23

for j being Nat
for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg ((f /. j),p) holds
LE q,p, L~ f,f /. 1,f /. (len f)