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 A1: ( 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 ) ; :: 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 A2: 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 )
assume A3: ( 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 A4: B_Cut f,p,q = R_Cut (L_Cut f,p),q by A1, JORDAN3:def 8;
A5: ( 1 <= Index q,f & Index q,f < len f ) by A1, JORDAN3:41;
Index p,f < len f by A1, JORDAN3:41;
then A6: (Index p,f) + 1 <= len f by NAT_1:13;
A7: 1 < len f by A5, XXREAL_0:2;

A9: 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 A3;

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

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

end;

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

A12: now

assume A13: p = f . ((Index p,f) + 1) ; :: thesis: contradiction
then A14: p = f /. ((Index p,f) + 1) by A6, FINSEQ_4:24, NAT_1:11;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A11, 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
A15: ( 0 <= r & r <= 1 ) ;
A17: 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 A11, A14, A15, A16, JORDAN3:def 6;
then r = 1 by A15, XXREAL_0:1;
hence contradiction by A1, A6, A13, A16, A17, FINSEQ_4:24, NAT_1:11; :: thesis: verum

end;

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

end;

end;

end;

then A18: L_Cut f,p is_S-Seq_joining p,f /. (len f) by A1, A2, Th40;

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 A3;

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 A1, 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 A1, 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 A19: q in L~ (L_Cut f,p) by SPPOL_2:17;
then ( 1 <= Index q,(L_Cut f,p) & Index q,(L_Cut f,p) < len (L_Cut f,p) ) by JORDAN3:41;
then A20: 1 <= len (L_Cut f,p) by XXREAL_0:2;
A21: (L_Cut f,p) . 1 = p by A18, JORDAN3:def 3;
then p = (L_Cut f,p) /. 1 by A20, FINSEQ_4:24;
hence B_Cut f,p,q is_S-Seq_joining p,q by A1, A2, A4, A9, A19, A21, Th42, JORDAN3:67; :: thesis: verum