let f be S-Sequence_in_R2; :: thesis: for p being Point of ()
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)

let p be Point of (); :: thesis: 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)

let j be Nat; :: thesis: ( 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) implies LE f /. j,p, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in L~ (mid (f,j,(len f))) ; :: thesis: LE f /. j,p, L~ f,f /. 1,f /. (len f)
consider i being Nat such that
A4: 1 <= i and
A5: i + 1 <= len (mid (f,j,(len f))) and
A6: p in LSeg ((mid (f,j,(len f))),i) by ;
A7: len (mid (f,j,(len f))) = ((len f) -' j) + 1 by ;
then i <= (len f) -' j by ;
then A8: i + j <= len f by ;
j + i >= i by NAT_1:11;
then A9: ((j + i) -' 1) + 1 <= len f by ;
1 + 1 <= j + i by ;
then A10: 1 <= (j + i) -' 1 by NAT_D:49;
j + 1 <= j + i by ;
then A11: j <= (j + i) -' 1 by NAT_D:49;
((j + i) -' 1) + 1 >= (j + i) -' 1 by NAT_1:11;
then len f >= (j + i) -' 1 by ;
then A12: LE f /. j,f /. ((j + i) -' 1), L~ f,f /. 1,f /. (len f) by ;
i < ((len f) -' j) + 1 by ;
then p in LSeg (f,((j + i) -' 1)) by ;
then LE f /. ((j + i) -' 1),p, L~ f,f /. 1,f /. (len f) by ;
hence LE f /. j,p, L~ f,f /. 1,f /. (len f) by ; :: thesis: verum