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. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> 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. & len f <> 2 & p in L~ f & q in L~ f & p <> q & p <> f . 1 & q <> 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: len f <> 2 and
A3: p in L~ f and
A4: q in L~ f and
A5: p <> q and
A6: p <> f . 1 and
A7: q <> f . 1 ; :: 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, A3, A4, A5, A6, Lm1; :: thesis: verum

end;

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

A9: now

assume that
A10: Index p,f = Index q,f and
A11: 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)
A12: Index p,f < len f by A3, JORDAN3:41;
A13: 1 <= Index p,f by A3, JORDAN3:41;
then A14: Index p,f in dom f by A12, FINSEQ_3:27;
f is weakly-one-to-one by A1, A2, Th7;
then f . (Index p,f) <> f . ((Index p,f) + 1) by A13, A12, Def2;
then A15: f /. (Index p,f) <> f . ((Index p,f) + 1) by A14, PARTFUN1:def 8;
A16: (Index p,f) + 1 <= len f by A12, NAT_1:13;
then A17: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A13, TOPREAL1:def 5;
then A18: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A3, JORDAN3:42;
1 <= (Index p,f) + 1 by NAT_1:11;
then (Index p,f) + 1 in dom f by A16, FINSEQ_3:27;
then A19: f /. (Index p,f) <> f /. ((Index p,f) + 1) by A15, PARTFUN1:def 8;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A4, A10, A17, JORDAN3:42;
then LT q,p,f /. (Index p,f),f /. ((Index p,f) + 1) by A11, A18, A19, JORDAN3:63;
hence LE q,p,f /. (Index q,f),f /. ((Index q,f) + 1) by A10, JORDAN3:def 7; :: thesis: verum

end;

A20: ( 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 A8, XXREAL_0:1;
B_Cut f,p,q = Rev (R_Cut (L_Cut f,q),p) by A8, JORDAN3:def 8;
then A21: Rev (B_Cut f,q,p) = B_Cut f,p,q by A3, A4, A20, A9, JORDAN3:def 8;
B_Cut f,q,p is_S-Seq_joining q,p by A1, A3, A4, A5, A7, A20, A9, Lm1;
hence B_Cut f,p,q is_S-Seq_joining p,q by A21, JORDAN3:48; :: thesis: verum

end;

end;