theorem Th3: :: SPRECT_4:3

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