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. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( 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) ) ) holds
B_Cut (f,p,q) is_S-Seq_joining p,q
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. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( 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) ) ) 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:
p in L~ f
and
A3:
q in L~ f
and
A4:
p <> q
; ( not 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) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q )
assume A5:
p <> f . 1
; ( ( 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) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q )
A6:
Index (q,f) < len f
by A3, JORDAN3:8;
Index (p,f) < len f
by A2, JORDAN3:8;
then A7:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
assume A8:
( 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) ) )
; B_Cut (f,p,q) is_S-Seq_joining p,q
then A9:
B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q)
by A2, A3, JORDAN3:def 7;
1 <= Index (q,f)
by A3, JORDAN3:8;
then A10:
1 < len f
by A6, XXREAL_0:2;
A11:
now ( ( Index (p,f) < Index (q,f) & not p = f . (len f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & not p = f . (len f) ) )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) ) )
by A8;
case A14:
(
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) )
;
not p = f . (len f)A15:
now not p = f . ((Index (p,f)) + 1)
q in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A14, JORDAN3:def 5;
then consider r being
Real such that A16:
q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1)))
and A17:
0 <= r
and A18:
r <= 1
;
A19:
p =
1
* p
by RLVECT_1:def 8
.=
(0. (TOP-REAL 2)) + (1 * p)
by RLVECT_1:4
.=
((1 - 1) * (f /. (Index (p,f)))) + (1 * p)
by RLVECT_1:10
;
assume A20:
p = f . ((Index (p,f)) + 1)
;
contradictionthen
p = f /. ((Index (p,f)) + 1)
by A7, FINSEQ_4:15, NAT_1:11;
then
1
<= r
by A14, A16, A17, A19, JORDAN3:def 5;
then
r = 1
by A18, XXREAL_0:1;
hence
contradiction
by A4, A7, A20, A16, A19, FINSEQ_4:15, NAT_1:11;
verum end; assume
p = f . (len f)
;
contradictionhence
contradiction
by A1, A10, A15, Th18;
verum end; end; end;
then
L_Cut (f,p) is_S-Seq_joining p,f /. (len f)
by A1, A2, A5, Th40;
then A21:
(L_Cut (f,p)) . 1 = p
by JORDAN3:def 2;
now ( ( Index (p,f) < Index (q,f) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) )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) ) )
by A8;
case
(
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) )
;
ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) )end; end; end;
then A22:
q in L~ (L_Cut (f,p))
by SPPOL_2:17;
then A23:
Index (q,(L_Cut (f,p))) < len (L_Cut (f,p))
by JORDAN3:8;
1 <= Index (q,(L_Cut (f,p)))
by A22, JORDAN3:8;
then
1 <= len (L_Cut (f,p))
by A23, XXREAL_0:2;
then
p = (L_Cut (f,p)) /. 1
by A21, FINSEQ_4:15;
hence
B_Cut (f,p,q) is_S-Seq_joining p,q
by A1, A2, A4, A5, A9, A11, A22, A21, Th42, JORDAN3:32; verum