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 A1: ( f is being_S-Seq & p in L~ f & q in L~ f & 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 A2: ( 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 A3: B_Cut f,p,q = R_Cut (L_Cut f,p),q by A1, Def8;
A4: ( 1 <= Index q,f & Index q,f < len f ) by A1, Th41;
Index p,f < len f by A1, Th41;
then A5: (Index p,f) + 1 <= len f by NAT_1:13;
A6: 1 < len f by A4, XXREAL_0:2;

A7: 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 A2;

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

then A8: (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, A6, A8, Th45;
hence contradiction by A1, Th41; :: thesis: verum

end;

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

A10: now

assume A11: p = f . ((Index p,f) + 1) ; :: thesis: contradiction
then A12: p = f /. ((Index p,f) + 1) by A5, FINSEQ_4:24, NAT_1:11;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A9, Def6;
then consider r being Real such that
A13: ( 0 <= r & r <= 1 ) and
A14: q = ((1 - r) * (f /. (Index p,f))) + (r * (f /. ((Index p,f) + 1))) by SPPOL_1:21;
A15: p = 1 * p by EUCLID:33
.= (0.REAL 2) + (1 * p) by EUCLID:31
.= ((1 - 1) * (f /. (Index p,f))) + (1 * p) by EUCLID:33 ;
then 1 <= r by A9, A12, A13, A14, Def6;
then r = 1 by A13, XXREAL_0:1;
hence contradiction by A1, A5, A11, A14, A15, FINSEQ_4:24, NAT_1:11; :: thesis: verum

end;

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

end;

end;

end;

then A16: L_Cut f,p is_S-Seq_joining p,f /. (len f) by A1, Th68;

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

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, 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 A1, 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 A17: 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 Th41;
then A18: 1 <= len (L_Cut f,p) by XXREAL_0:2;
A19: (L_Cut f,p) . 1 = p by A16, Def3;
then p = (L_Cut f,p) /. 1 by A18, FINSEQ_4:24;
hence B_Cut f,p,q is_S-Seq_joining p,q by A1, A3, A7, A17, A19, Th67, Th69; :: thesis: verum