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:8;
Index (p,f) < len f by A2, JORDAN3:8;
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 7;
1 <= Index (q,f) by A3, JORDAN3:8;
then A10: 1 < len f by A6, XXREAL_0:2;

A11: now :: thesis: ( ( Index (p,f) < Index (q,f) & not p = f . (len f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & not p = f . (len f) ) )

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:8; :: 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 :: thesis: not p = f . ((Index (p,f)) + 1)

q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A14, JORDAN3:def 5;
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 RLVECT_1:def 8
.= (0. (TOP-REAL 2)) + (1 * p) by RLVECT_1:4
.= ((1 - 1) * (f /. (Index (p,f)))) + (1 * p) by RLVECT_1:10 ;
assume A20: p = f . ((Index (p,f)) + 1) ; :: thesis: contradiction
then p = f /. ((Index (p,f)) + 1) by A7, FINSEQ_4:15, NAT_1:11;
then 1 <= r by A14, A16, A17, A19, JORDAN3:def 5;
then r = 1 by A18, XXREAL_0:1;
hence contradiction by A4, A7, A20, A16, A19, FINSEQ_4:15, 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 2;

now :: thesis: ( ( Index (p,f) < Index (q,f) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) )

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 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:29;
hence ex i1 being 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 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:31;
hence ex i1 being 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:8;
1 <= Index (q,(L_Cut (f,p))) by A22, JORDAN3:8;
then 1 <= len (L_Cut (f,p)) by A23, XXREAL_0:2;
then p = (L_Cut (f,p)) /. 1 by A21, FINSEQ_4:15;
hence B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A4, A5, A9, A11, A22, A21, Th42, JORDAN3:32; :: thesis: verum