let f be FinSequence of (TOP-REAL 2); :: thesis:
let p, q be Point of (TOP-REAL 2); :: thesis:
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: p <> q and
A4: Index p,f = Index q,f and
A5: LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ; :: thesis:
set i1 = ((Index q,f) -' (Index p,f)) + 1;
A6: ( 1 <= Index q,f & Index q,f < len f ) by A2, Th41;
Index q,f < len f by A2, Th41;
then A7: (Index q,f) + 1 <= len f by NAT_1:13;
A8: (Index q,f) -' (Index p,f) = (Index q,f) - (Index p,f) by A4, XREAL_1:235
.= 0 by A4 ;
1 < (0 + 1) + 1 ;
then A9: len <*p*> < (((Index q,f) -' (Index p,f)) + 1) + 1 by A8, FINSEQ_1:57;
A10: 1 <= (Index p,f) + 1 by NAT_1:11;
1 < len f by A6, XXREAL_0:2;
then len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1 by A4, A7, A10, Th27;
then A11: (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) = 1 + (((len f) -' ((Index p,f) + 1)) + 1) by FINSEQ_1:57
.= 1 + (((len f) - ((Index p,f) + 1)) + 1) by A4, A7, XREAL_1:235
.= ((len f) - (Index p,f)) + 1 ;
(Index q,f) - (Index p,f) <= (len f) - (Index p,f) by A6, XREAL_1:11;
then A12: ((Index q,f) - (Index p,f)) + 1 <= ((len f) - (Index p,f)) + 1 by XREAL_1:8;

A13: now

assume A14: p = f . ((Index p,f) + 1) ; :: thesis:
then A15: p = f /. ((Index p,f) + 1) by A4, A7, FINSEQ_4:24, NAT_1:11;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A5, Def6;
then consider r being Real such that
A17: q = ((1 - r) * (f /. (Index p,f))) + (r * (f /. ((Index p,f) + 1))) and
A16: ( 0 <= r & r <= 1 ) ;
A18: p = 1 * p by EUCLID:33
.= (0. (TOP-REAL 2)) + (1 * p) by EUCLID:31
.= ((1 - 1) * (f /. (Index p,f))) + (1 * p) by EUCLID:33 ;
then 1 <= r by A5, A15, A16, A17, Def6;
then r = 1 by A16, XXREAL_0:1;
hence contradiction by A3, A4, A7, A14, A17, A18, FINSEQ_4:24, NAT_1:11; :: thesis:

end;

then A19: len (L_Cut f,p) = ((len f) - (Index p,f)) + 1 by A1, Th61;
then A20: (L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) = (L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1) by A4, A8, A12, FINSEQ_4:24
.= (<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . (((Index q,f) -' (Index p,f)) + 1) by A13, Def4
.= p by A8, FINSEQ_1:58 ;
A21: Index q,f < len f by A2, Th41;
then A22: (Index q,f) + 1 <= len f by NAT_1:13;
then ((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f) by XREAL_1:11;
then ((Index q,f) - (Index p,f)) + 1 <= (len f) - (Index p,f) ;
then ((Index q,f) -' (Index p,f)) + 1 <= (len f) - (Index p,f) by A4, XREAL_0:def 2;
then A23: (((Index q,f) -' (Index p,f)) + 1) + 1 <= len (L_Cut f,p) by A19, XREAL_1:8;
A24: ( 1 <= Index q,f & (Index q,f) + 1 <= len f & q in LSeg f,(Index q,f) ) by A2, A21, Th41, Th42, NAT_1:13;
A25: ((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f) by A22, XREAL_1:11;
then A26: (((Index q,f) - (Index p,f)) + 1) + 1 <= ((len f) - (Index p,f)) + 1 by XREAL_1:8;
then A27: (((Index q,f) -' (Index p,f)) + 1) + 1 <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) by A4, A11, XREAL_1:235;
((Index q,f) - (Index p,f)) + 1 <= (len f) - (Index p,f) by A25;
then A28: ((Index q,f) -' (Index p,f)) + 1 <= ((len f) - ((Index p,f) + 1)) + 1 by A4, XREAL_1:235;
A29: ( 1 <= (Index q,f) + 1 & (Index q,f) + 1 <= len f ) by A24, NAT_D:48;
(L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1) = (L_Cut f,p) . ((((Index q,f) -' (Index p,f)) + 1) + 1) by A4, A8, A19, A26, FINSEQ_4:24
.= (<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . ((((Index q,f) -' (Index p,f)) + 1) + 1) by A13, Def4
.= (mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - (len <*p*>)) by A9, A27, Th15
.= (mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - 1) by FINSEQ_1:57
.= f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1) by A4, A7, A8, A10, A28, Th31
.= f /. ((Index q,f) + 1) by A29, FINSEQ_4:24 ;
then q in LSeg ((L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1)),((L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1)) by A4, A5, A20, Th65;
hence q in L~ (L_Cut f,p) by A8, A23, SPPOL_2:15; :: thesis: