let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q & ( 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 being_S-Seq & p in L~ f & q in L~ f & p <> q & ( 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 being_S-Seq and
A2: p in L~ f and
A3: q in L~ f and
A4: p <> q ; :: 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 A5: ( 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 A6: B_Cut f,p,q = R_Cut (L_Cut f,p),q by A2, A3, Def8;
Index p,f < len f by A2, Th41;
then A7: (Index p,f) + 1 <= len f by NAT_1:13;
A8: Index q,f < len f by A3, Th41;
1 <= Index q,f by A3, Th41;
then A9: 1 < len f by A8, XXREAL_0:2;

A10: 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 A5;

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

assume A12: p = f . (len f) ; :: thesis: contradiction
(Index p,f) + 1 <= Index q,f by A11, NAT_1:13;
then len f <= Index q,f by A1, A9, A12, Th45;
hence contradiction by A3, Th41; :: thesis: verum

end;

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

A14: now

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

end;

assume p = f . (len f) ; :: thesis: contradiction
hence contradiction by A1, A9, A14, Th45; :: thesis: verum

end;

end;

end;

then L_Cut f,p is_S-Seq_joining p,f /. (len f) by A1, A2, Th68;
then A20: (L_Cut f,p) . 1 = p by Def3;

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

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, Th64;
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, Th66;
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 A21: q in L~ (L_Cut f,p) by SPPOL_2:17;
then A22: Index q,(L_Cut f,p) < len (L_Cut f,p) by Th41;
1 <= Index q,(L_Cut f,p) by A21, Th41;
then 1 <= len (L_Cut f,p) by A22, XXREAL_0:2;
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, A6, A10, A21, A20, Th67, Th69; :: thesis: verum