let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds
p in L~ (L_Cut f,q)
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq implies p in L~ (L_Cut f,q) )
assume A1: ( p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq ) ; :: thesis: p in L~ (L_Cut f,q)
then 1 + 1 <= len f by TOPREAL1:def 10;
then A2: 1 < len f by XXREAL_0:2;
then A3: (Index p,f) + 1 = len f by A1, JORDAN3:45;
Index q,f < len f by A1, JORDAN3:41;
then A4: Index q,f <= Index p,f by A3, NAT_1:13;

per cases ( Index q,f = Index p,f or Index q,f < Index p,f ) by A4, XXREAL_0:1;

suppose Index q,f = Index p,f ; :: thesis: p in L~ (L_Cut f,q)

then A5: L_Cut f,q = <*q*> ^ (mid f,(len f),(len f)) by A1, A3, JORDAN3:def 4
.= <*q*> ^ <*(f /. (len f))*> by A2, JORDAN4:27
.= <*q,(f /. (len f))*> by FINSEQ_1:def 9
.= <*q,p*> by A1, A2, FINSEQ_4:24 ;
then rng (L_Cut f,q) = {p,q} by FINSEQ_2:147;
then A6: p in rng (L_Cut f,q) by TARSKI:def 2;
len (L_Cut f,q) = 2 by A5, FINSEQ_1:61;
then rng (L_Cut f,q) c= L~ (L_Cut f,q) by SPPOL_2:18;
hence p in L~ (L_Cut f,q) by A6; :: thesis: verum

end;

suppose Index q,f < Index p,f ; :: thesis: p in L~ (L_Cut f,q)

hence p in L~ (L_Cut f,q) by A1, JORDAN3:64; :: thesis: verum

end;

end;