let f be FinSequence of (TOP-REAL 2); for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q & ( 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 being_S-Seq & p in L~ f & q in L~ f & p <> q & ( 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 being_S-Seq
and
A2:
p in L~ f
and
A3:
q in L~ f
and
A4:
p <> q
; ( ( 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:
( 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 A6:
B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q)
by A2, A3, Def7;
Index (p,f) < len f
by A2, Th8;
then A7:
(Index (p,f)) + 1 <= len f
by NAT_1:13;
A8:
Index (q,f) < len f
by A3, Th8;
1 <= Index (q,f)
by A3, Th8;
then A9:
1 < len f
by A8, XXREAL_0:2;
A10:
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 A5;
case A13:
(
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) )
;
not p = f . (len f)A14:
now not p = f . ((Index (p,f)) + 1)
q in LSeg (
(f /. (Index (p,f))),
(f /. ((Index (p,f)) + 1)))
by A13;
then consider r being
Real such that A15:
q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1)))
and A16:
0 <= r
and A17:
r <= 1
;
A18:
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 A19:
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 A13, A15, A16, A18;
then
r = 1
by A17, XXREAL_0:1;
hence
contradiction
by A4, A7, A19, A15, A18, FINSEQ_4:15, NAT_1:11;
verum end; assume
p = f . (len f)
;
contradictionhence
contradiction
by A1, A9, A14, Th12;
verum end; end; end;
then
L_Cut (f,p) is_S-Seq_joining p,f /. (len f)
by A1, A2, Th33;
then A20:
(L_Cut (f,p)) . 1 = p
;
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 A5;
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 A21:
q in L~ (L_Cut (f,p))
by SPPOL_2:17;
then A22:
Index (q,(L_Cut (f,p))) < len (L_Cut (f,p))
by Th8;
1 <= Index (q,(L_Cut (f,p)))
by A21, Th8;
then
1 <= len (L_Cut (f,p))
by A22, XXREAL_0:2;
then
p = (L_Cut (f,p)) /. 1
by A20, FINSEQ_4:15;
hence
B_Cut (f,p,q) is_S-Seq_joining p,q
by A1, A2, A4, A6, A10, A21, A20, Th32, Th34; verum