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 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 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: B_Cut f,p,q is_S-Seq_joining p,q

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

suppose ( 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

hence B_Cut f,p,q is_S-Seq_joining p,q by A1, Lm1; :: thesis: verum

end;

suppose A2: ( 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) ) ) ; :: thesis: B_Cut f,p,q is_S-Seq_joining p,q

then A3: B_Cut f,p,q = Rev (R_Cut (L_Cut f,q),p) by Def8;
A4: ( Index q,f < Index p,f or ( Index p,f = Index q,f & not LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) by A2, XXREAL_0:1;

A5: now

assume that
A6: Index p,f = Index q,f and
A7: not LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ; :: thesis: LE q,p,f /. (Index q,f),f /. ((Index q,f) + 1)
A8: 1 <= Index p,f by A1, Th41;
A9: Index p,f < len f by A1, Th41;
then A10: (Index p,f) + 1 <= len f by NAT_1:13;
then A11: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A8, TOPREAL1:def 5;
then A12: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, Th42;
A13: q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, A6, A11, Th42;
A14: Index p,f in dom f by A8, A9, FINSEQ_3:27;
1 <= (Index p,f) + 1 by NAT_1:11;
then A15: (Index p,f) + 1 in dom f by A10, FINSEQ_3:27;
A16: (Index p,f) + 0 <> (Index p,f) + 1 ;
f is one-to-one by A1;
then f /. (Index p,f) <> f /. ((Index p,f) + 1) by A14, A15, A16, PARTFUN2:17;
then LT q,p,f /. (Index p,f),f /. ((Index p,f) + 1) by A7, A12, A13, Th63;
hence LE q,p,f /. (Index q,f),f /. ((Index q,f) + 1) by A6, Def7; :: thesis: verum

end;

then A17: B_Cut f,q,p is_S-Seq_joining q,p by A1, A4, Lm1;
Rev (B_Cut f,q,p) = B_Cut f,p,q by A1, A3, A4, A5, Def8;
hence B_Cut f,p,q is_S-Seq_joining p,q by A17, Th48; :: thesis: verum

end;

end;