let f be FinSequence of (TOP-REAL 2); 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); ( 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 that
A1:
p in L~ f
and
A2:
q in L~ f
and
A3:
q <> f . (len f)
and
A4:
p = f . (len f)
and
A5:
f is being_S-Seq
; p in L~ (L_Cut f,q)
1 + 1 <= len f
by A5, TOPREAL1:def 10;
then A6:
1 < len f
by XXREAL_0:2;
then A7:
(Index p,f) + 1 = len f
by A4, A5, JORDAN3:45;
Index q,f < len f
by A2, JORDAN3:41;
then A8:
Index q,f <= Index p,f
by A7, NAT_1:13;
per cases
( Index q,f = Index p,f or Index q,f < Index p,f )
by A8, XXREAL_0:1;
suppose
Index q,
f = Index p,
f
;
p in L~ (L_Cut f,q)then A9:
L_Cut f,
q =
<*q*> ^ (mid f,(len f),(len f))
by A3, A7, JORDAN3:def 4
.=
<*q*> ^ <*(f /. (len f))*>
by A6, JORDAN4:27
.=
<*q,(f /. (len f))*>
by FINSEQ_1:def 9
.=
<*q,p*>
by A4, A6, FINSEQ_4:24
;
then
rng (L_Cut f,q) = {p,q}
by FINSEQ_2:147;
then A10:
p in rng (L_Cut f,q)
by TARSKI:def 2;
len (L_Cut f,q) = 2
by A9, 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 A10;
verum end;