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 A1:
( 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_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,qend; 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,qthen A3:
B_Cut f,
p,
q = Rev (R_Cut (L_Cut f,q),p)
by JORDAN3:def 8;
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, JORDAN3:41;
A9:
Index p,
f < len f
by A1, JORDAN3:41;
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, JORDAN3:42;
A13:
q in LSeg (f /. (Index p,f)),
(f /. ((Index p,f) + 1))
by A1, A6, A11, JORDAN3:42;
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;
f is
weakly-one-to-one
by A1, Th7;
then
f . (Index p,f) <> f . ((Index p,f) + 1)
by A8, A9, Def2;
then
f /. (Index p,f) <> f . ((Index p,f) + 1)
by A14, PARTFUN1:def 8;
then
f /. (Index p,f) <> f /. ((Index p,f) + 1)
by A15, PARTFUN1:def 8;
then
LT q,
p,
f /. (Index p,f),
f /. ((Index p,f) + 1)
by A7, A12, A13, JORDAN3:63;
hence
LE q,
p,
f /. (Index q,f),
f /. ((Index q,f) + 1)
by A6, JORDAN3:def 7;
:: thesis: verum end; then A16:
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, JORDAN3:def 8;
hence
B_Cut f,
p,
q is_S-Seq_joining p,
q
by A16, JORDAN3:48;
:: thesis: verum end;