let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) holds
B_Cut f,p,q is_S-Seq_joining p,q
let p, q be Point of (TOP-REAL 2); :: thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) implies B_Cut f,p,q is_S-Seq_joining p,q )
assume that
A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: q in L~ f and
A4: p <> q ; :: thesis: ( not p <> f . 1 or ( not Index p,f < Index q,f & not ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) or B_Cut f,p,q is_S-Seq_joining p,q )
assume A5: p <> f . 1 ; :: thesis: ( ( not Index p,f < Index q,f & not ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) or B_Cut f,p,q is_S-Seq_joining p,q )
A6: Index q,f < len f by A3, JORDAN3:41;
Index p,f < len f by A2, JORDAN3:41;
then A7: (Index p,f) + 1 <= len f by NAT_1:13;
assume A8: ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) ; :: thesis: B_Cut f,p,q is_S-Seq_joining p,q
then A9: B_Cut f,p,q = R_Cut (L_Cut f,p),q by A2, A3, JORDAN3:def 8;
1 <= Index q,f by A3, JORDAN3:41;
then A10: 1 < len f by A6, XXREAL_0:2;

A11: now

per cases ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) by A8;

case A12: Index p,f < Index q,f ; :: thesis: not p = f . (len f)

assume A13: p = f . (len f) ; :: thesis: contradiction
(Index p,f) + 1 <= Index q,f by A12, NAT_1:13;
then len f <= Index q,f by A1, A10, A13, Th18;
hence contradiction by A3, JORDAN3:41; :: thesis: verum

end;

case A14: ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ; :: thesis: not p = f . (len f)

A15: now

q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A14, JORDAN3:def 6;
then consider r being Real such that
A16: q = ((1 - r) * (f /. (Index p,f))) + (r * (f /. ((Index p,f) + 1))) and
A17: 0 <= r and
A18: r <= 1 ;
A19: 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 ;
assume A20: p = f . ((Index p,f) + 1) ; :: thesis: contradiction
then p = f /. ((Index p,f) + 1) by A7, FINSEQ_4:24, NAT_1:11;
then 1 <= r by A14, A16, A17, A19, JORDAN3:def 6;
then r = 1 by A18, XXREAL_0:1;
hence contradiction by A4, A7, A20, A16, A19, FINSEQ_4:24, NAT_1:11; :: thesis: verum

end;

assume p = f . (len f) ; :: thesis: contradiction
hence contradiction by A1, A10, A15, Th18; :: thesis: verum

end;

end;

end;

then L_Cut f,p is_S-Seq_joining p,f /. (len f) by A1, A2, A5, Th40;
then A21: (L_Cut f,p) . 1 = p by JORDAN3:def 3;

now

per cases ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) by A8;

case Index p,f < Index q,f ; :: thesis: ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 )

then q in L~ (L_Cut f,p) by A2, A3, JORDAN3:64;
hence ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 ) by SPPOL_2:13; :: thesis: verum

end;

case ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ; :: thesis: ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 )

then q in L~ (L_Cut f,p) by A2, A3, A4, JORDAN3:66;
hence ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 ) by SPPOL_2:13; :: thesis: verum

end;

end;

end;

then A22: q in L~ (L_Cut f,p) by SPPOL_2:17;
then A23: Index q,(L_Cut f,p) < len (L_Cut f,p) by JORDAN3:41;
1 <= Index q,(L_Cut f,p) by A22, JORDAN3:41;
then 1 <= len (L_Cut f,p) by A23, XXREAL_0:2;
then p = (L_Cut f,p) /. 1 by A21, FINSEQ_4:24;
hence B_Cut f,p,q is_S-Seq_joining p,q by A1, A2, A4, A5, A9, A11, A22, A21, Th42, JORDAN3:67; :: thesis: verum