let f be non empty FinSequence of (TOP-REAL 2); 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); ( 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 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
; B_Cut (f,p,q) is being_S-Seq
B_Cut (f,p,q) is_S-Seq_joining p,q
by A1, A2, A3, A4, A5, A6, A7, Th43;
hence
B_Cut (f,p,q) is being_S-Seq
by JORDAN3:def 2; verum