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 being_S-Seq
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 being_S-Seq )
assume ( 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 ) ; :: thesis: B_Cut f,p,q is being_S-Seq
then B_Cut f,p,q is_S-Seq_joining p,q by Th43;
hence B_Cut f,p,q is being_S-Seq by JORDAN3:def 3; :: thesis: verum