let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2)
for r being Real
for u being Point of (Euclid 2) st not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & f is being_S-Seq & not p in L~ f holds
ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
let f be FinSequence of (TOP-REAL 2); :: thesis: for r being Real
for u being Point of (Euclid 2) st not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & f is being_S-Seq & not p in L~ f holds
ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
let r be Real; :: thesis: for u being Point of (Euclid 2) st not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & f is being_S-Seq & not p in L~ f holds
ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
let u be Point of (Euclid 2); :: thesis: ( not f /. 1 in Ball u,r & f /. (len f) in Ball u,r & p in Ball u,r & f is being_S-Seq & not p in L~ f implies ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) ) )
set p1 = f /. 1;
set Mf = { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ;
assume that
A1:
not f /. 1 in Ball u,r
and
A2:
f /. (len f) in Ball u,r
and
A3:
p in Ball u,r
and
A4:
f is being_S-Seq
and
A5:
not p in L~ f
; :: thesis: ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
A6:
f is special
by A4, TOPREAL1:def 10;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len f) - 1 & LSeg f,$1 meets Ball u,r );
A7:
len f >= 2
by A4, TOPREAL1:def 10;
then reconsider n = (len f) - 1 as Element of NAT by INT_1:18, XXREAL_0:2;
2 = 1 + 1
;
then A8:
1 <= (len f) - 1
by A7, XREAL_1:21;
n + 1 = len f
;
then
f /. (len f) in LSeg f,n
by A8, TOPREAL1:27;
then
LSeg f,n meets Ball u,r
by A2, XBOOLE_0:3;
then A9:
ex n being Nat st S1[n]
by A8;
consider m being Nat such that
A10:
S1[m]
and
A11:
for i being Nat st S1[i] holds
m <= i
from NAT_1:sch 5(A9);
reconsider m = m as Element of NAT by ORDINAL1:def 13;
consider q1, q2 being Point of (TOP-REAL 2) such that
A12:
f /. m = q1
and
A13:
f /. (m + 1) = q2
;
A14:
(LSeg f,m) /\ (Ball u,r) <> {}
by A10, XBOOLE_0:def 7;
A15:
m + 1 <= len f
by A10, XREAL_1:21;
then A16:
LSeg f,m = LSeg q1,q2
by A10, A12, A13, TOPREAL1:def 5;
m <= m + 1
by NAT_1:11;
then A17:
m <= len f
by A15, XXREAL_0:2;
A18:
Seg (len f) = dom f
by FINSEQ_1:def 3;
A19:
now consider x being
Element of
(Ball u,r) /\ (L~ (f | m));
set M =
{ (LSeg (f | m),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | m) ) } ;
A20:
Seg (len (f | m)) = dom (f | m)
by FINSEQ_1:def 3;
assume A21:
(Ball u,r) /\ (L~ (f | m)) <> {}
;
:: thesis: contradictionthen A22:
x in Ball u,
r
by XBOOLE_0:def 4;
x in L~ (f | m)
by A21, XBOOLE_0:def 4;
then consider X being
set such that A23:
x in X
and A24:
X in { (LSeg (f | m),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | m) ) }
by TARSKI:def 4;
consider k being
Element of
NAT such that A25:
X = LSeg (f | m),
k
and A26:
1
<= k
and A27:
k + 1
<= len (f | m)
by A24;
k <= k + 1
by NAT_1:11;
then
k <= len (f | m)
by A27, XXREAL_0:2;
then A28:
k in Seg (len (f | m))
by A26, FINSEQ_1:3;
1
<= k + 1
by NAT_1:11;
then
k + 1
in Seg (len (f | m))
by A27, FINSEQ_1:3;
then
x in LSeg f,
k
by A23, A25, A28, A20, TOPREAL3:24;
then A29:
LSeg f,
k meets Ball u,
r
by A22, XBOOLE_0:3;
Seg m c= Seg (len f)
by A17, FINSEQ_1:7;
then A30:
Seg m =
(dom f) /\ (Seg m)
by A18, XBOOLE_1:28
.=
dom (f | (Seg m))
by RELAT_1:90
.=
Seg (len (f | m))
by A20, FINSEQ_1:def 15
;
A31:
(k + 1) - 1
<= (len (f | m)) - 1
by A27, XREAL_1:11;
then A32:
k <= m - 1
by A30, FINSEQ_1:8;
m = len (f | m)
by A30, FINSEQ_1:8;
then
(len (f | m)) - 1
<= (len f) - 1
by A17, XREAL_1:11;
then
k <= (len f) - 1
by A31, XXREAL_0:2;
then
m <= k
by A11, A26, A29;
then
m <= m - 1
by A32, XXREAL_0:2;
then
0 <= (m + (- 1)) - m
by XREAL_1:50;
hence
contradiction
;
:: thesis: verum end;
then A35:
not q1 in Ball u,r
by A1, A10, A12, TOPREAL3:33;
set A = (LSeg f,m) /\ (Ball u,r);
A36:
( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q2 `1 ),(q2 `2 )]| )
by EUCLID:57;
m + 1 <= n + 1
by A10, XREAL_1:8;
then
LSeg f,m in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) }
by A10;
then A37:
LSeg f,m c= union { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) }
by ZFMISC_1:92;
now per cases
( ex q being Point of (TOP-REAL 2) st
( q in (LSeg f,m) /\ (Ball u,r) & ( p `1 = q `1 or p `2 = q `2 ) ) or for q being Point of (TOP-REAL 2) st q in (LSeg f,m) /\ (Ball u,r) holds
( p `1 <> q `1 & p `2 <> q `2 ) )
;
suppose
ex
q being
Point of
(TOP-REAL 2) st
(
q in (LSeg f,m) /\ (Ball u,r) & (
p `1 = q `1 or
p `2 = q `2 ) )
;
:: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )then consider q being
Point of
(TOP-REAL 2) such that A38:
q in (LSeg f,m) /\ (Ball u,r)
and A39:
(
p `1 = q `1 or
p `2 = q `2 )
;
A40:
q in Ball u,
r
by A38, XBOOLE_0:def 4;
A41:
q in LSeg q,
p
by RLTOPSP1:69;
A42:
q in LSeg f,
m
by A38, XBOOLE_0:def 4;
then consider h being
FinSequence of
(TOP-REAL 2) such that A43:
h is
being_S-Seq
and A44:
h /. 1
= f /. 1
and A45:
h /. (len h) = q
and A46:
L~ h is_S-P_arc_joining f /. 1,
q
and A47:
L~ h c= L~ f
and A48:
L~ h = (L~ (f | m)) \/ (LSeg q1,q)
by A1, A4, A12, A40, Th18;
take g =
h ^ <*p*>;
:: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )A49:
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r)
by A47, XBOOLE_1:9;
A50:
q in L~ f
by A37, A42;
A52:
(LSeg q,p) /\ (L~ h) c= {q}
proof
LSeg q,
p = (LSeg q,p) /\ (Ball u,r)
by A3, A40, TOPREAL3:28, XBOOLE_1:28;
then A54:
(LSeg q,p) /\ ((L~ (f | m)) \/ (LSeg q1,q)) =
(((LSeg q,p) /\ (Ball u,r)) /\ (L~ (f | m))) \/ ((LSeg q,p) /\ (LSeg q1,q))
by XBOOLE_1:23
.=
((LSeg q,p) /\ ((Ball u,r) /\ (L~ (f | m)))) \/ ((LSeg q,p) /\ (LSeg q1,q))
by XBOOLE_1:16
.=
(LSeg q1,q) /\ (LSeg q,p)
by A19
;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (LSeg q,p) /\ (L~ h) or x in {q} )
assume
x in (LSeg q,p) /\ (L~ h)
;
:: thesis: x in {q}
hence
x in {q}
by A3, A35, A40, A51, A48, A54, A55, A53, TOPREAL3:49;
:: thesis: verum
end;
q in L~ h
by A46, Th4;
then
q in (LSeg q,p) /\ (L~ h)
by A41, XBOOLE_0:def 4;
then
{q} c= (LSeg q,p) /\ (L~ h)
by ZFMISC_1:37;
then A57:
(LSeg q,p) /\ (L~ h) = {q}
by A52, XBOOLE_0:def 10;
then
L~ g c= (L~ h) \/ (Ball u,r)
by A3, A40, A51, A43, A45, Th20;
hence
(
L~ g is_S-P_arc_joining f /. 1,
p &
L~ g c= (L~ f) \/ (Ball u,r) )
by A3, A40, A51, A43, A44, A45, A57, A49, Th20, XBOOLE_1:1;
:: thesis: verum end; suppose A58:
for
q being
Point of
(TOP-REAL 2) st
q in (LSeg f,m) /\ (Ball u,r) holds
(
p `1 <> q `1 &
p `2 <> q `2 )
;
:: thesis: ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )consider x being
Element of
(LSeg f,m) /\ (Ball u,r);
A59:
x in LSeg f,
m
by A14, XBOOLE_0:def 4;
then reconsider q =
x as
Point of
(TOP-REAL 2) ;
A60:
(
q `1 <> p `1 &
q `2 <> p `2 )
by A14, A58;
q <> f /. 1
by A1, A14, XBOOLE_0:def 4;
then consider h being
FinSequence of
(TOP-REAL 2) such that A61:
h is
being_S-Seq
and A62:
h /. 1
= f /. 1
and A63:
h /. (len h) = q
and A64:
L~ h is_S-P_arc_joining f /. 1,
q
and A65:
L~ h c= L~ f
and A66:
L~ h = (L~ (f | m)) \/ (LSeg q1,q)
by A4, A12, A59, Th18;
A67:
q in Ball u,
r
by A14, XBOOLE_0:def 4;
A68:
(
q = |[(q `1 ),(q `2 )]| &
p = |[(p `1 ),(p `2 )]| )
by EUCLID:57;
now per cases
( |[(q `1 ),(p `2 )]| in Ball u,r or |[(p `1 ),(q `2 )]| in Ball u,r )
by A3, A67, A68, TOPREAL3:32;
suppose A69:
|[(q `1 ),(p `2 )]| in Ball u,
r
;
:: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )set v =
|[(q `1 ),(p `2 )]|;
A70:
((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) c= {q}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) or x in {q} )
set L =
(LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p);
assume A71:
x in ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h)
;
:: thesis: x in {q}
(
LSeg q,
|[(q `1 ),(p `2 )]| c= Ball u,
r &
LSeg |[(q `1 ),(p `2 )]|,
p c= Ball u,
r )
by A3, A67, A69, TOPREAL3:28;
then
(LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p) = ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (Ball u,r)
by XBOOLE_1:8, XBOOLE_1:28;
then A72:
((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ ((L~ (f | m)) \/ (LSeg q1,q)) =
((((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (Ball u,r)) /\ (L~ (f | m))) \/ (((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (LSeg q1,q))
by XBOOLE_1:23
.=
(((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ ((Ball u,r) /\ (L~ (f | m)))) \/ (((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (LSeg q1,q))
by XBOOLE_1:16
.=
{} \/ (((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (LSeg q1,q))
by A19
;
now per cases
( q1 `1 = q `1 or q1 `2 = q `2 )
by A73;
suppose A74:
q1 `1 = q `1
;
:: thesis: x in {q}now
q1 in LSeg q1,
q2
by RLTOPSP1:69;
then A75:
LSeg q1,
q c= LSeg f,
m
by A16, A59, TOPREAL1:12;
A76:
|[(q `1 ),(p `2 )]| `2 = p `2
by EUCLID:56;
assume
|[(q `1 ),(p `2 )]| in LSeg q1,
q
;
:: thesis: contradictionthen
|[(q `1 ),(p `2 )]| in (LSeg f,m) /\ (Ball u,r)
by A69, A75, XBOOLE_0:def 4;
hence
contradiction
by A58, A76;
:: thesis: verum end; hence
x in {q}
by A35, A67, A60, A66, A69, A72, A71, A74, TOPREAL3:50;
:: thesis: verum
hence
x in {q}
;
:: thesis: verum
end; take g =
h ^ <*|[(q `1 ),(p `2 )]|,p*>;
:: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )
q in LSeg q,
|[(q `1 ),(p `2 )]|
by RLTOPSP1:69;
then A77:
q in (LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)
by XBOOLE_0:def 3;
A78:
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r)
by A65, XBOOLE_1:9;
q in L~ h
by A64, Th4;
then
q in ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h)
by A77, XBOOLE_0:def 4;
then
{q} c= ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h)
by ZFMISC_1:37;
then A79:
((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) = {q}
by A70, XBOOLE_0:def 10;
then
L~ g c= (L~ h) \/ (Ball u,r)
by A3, A67, A60, A61, A63, A69, Th22;
hence
(
L~ g is_S-P_arc_joining f /. 1,
p &
L~ g c= (L~ f) \/ (Ball u,r) )
by A3, A67, A60, A61, A62, A63, A69, A79, A78, Th22, XBOOLE_1:1;
:: thesis: verum end; suppose A80:
|[(p `1 ),(q `2 )]| in Ball u,
r
;
:: thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )set v =
|[(p `1 ),(q `2 )]|;
A81:
((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) c= {q}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) or x in {q} )
set L =
(LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p);
assume A82:
x in ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h)
;
:: thesis: x in {q}
(
LSeg q,
|[(p `1 ),(q `2 )]| c= Ball u,
r &
LSeg |[(p `1 ),(q `2 )]|,
p c= Ball u,
r )
by A3, A67, A80, TOPREAL3:28;
then
(LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p) = ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (Ball u,r)
by XBOOLE_1:8, XBOOLE_1:28;
then A83:
((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ ((L~ (f | m)) \/ (LSeg q1,q)) =
((((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (Ball u,r)) /\ (L~ (f | m))) \/ (((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (LSeg q1,q))
by XBOOLE_1:23
.=
(((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ ((Ball u,r) /\ (L~ (f | m)))) \/ (((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (LSeg q1,q))
by XBOOLE_1:16
.=
{} \/ (((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (LSeg q1,q))
by A19
;
now per cases
( q1 `1 = q `1 or q1 `2 = q `2 )
by A84;
suppose A85:
q1 `2 = q `2
;
:: thesis: x in {q}now
q1 in LSeg q1,
q2
by RLTOPSP1:69;
then A86:
LSeg q1,
q c= LSeg f,
m
by A16, A59, TOPREAL1:12;
A87:
|[(p `1 ),(q `2 )]| `1 = p `1
by EUCLID:56;
assume
|[(p `1 ),(q `2 )]| in LSeg q1,
q
;
:: thesis: contradictionthen
|[(p `1 ),(q `2 )]| in (LSeg f,m) /\ (Ball u,r)
by A80, A86, XBOOLE_0:def 4;
hence
contradiction
by A58, A87;
:: thesis: verum end; hence
x in {q}
by A35, A67, A60, A66, A80, A83, A82, A85, TOPREAL3:51;
:: thesis: verum
hence
x in {q}
;
:: thesis: verum
end; take g =
h ^ <*|[(p `1 ),(q `2 )]|,p*>;
:: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )
q in LSeg q,
|[(p `1 ),(q `2 )]|
by RLTOPSP1:69;
then A88:
q in (LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)
by XBOOLE_0:def 3;
A89:
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r)
by A65, XBOOLE_1:9;
q in L~ h
by A64, Th4;
then
q in ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h)
by A88, XBOOLE_0:def 4;
then
{q} c= ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h)
by ZFMISC_1:37;
then A90:
((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) = {q}
by A81, XBOOLE_0:def 10;
then
L~ g c= (L~ h) \/ (Ball u,r)
by A3, A67, A60, A61, A63, A80, Th21;
hence
(
L~ g is_S-P_arc_joining f /. 1,
p &
L~ g c= (L~ f) \/ (Ball u,r) )
by A3, A67, A60, A61, A62, A63, A80, A90, A89, Th21, XBOOLE_1:1;
:: thesis: verum end; hence
ex
h being
FinSequence of
(TOP-REAL 2) st
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball u,r) )
;
:: thesis: verum end;
hence
ex h being FinSequence of (TOP-REAL 2) st
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball u,r) )
; :: thesis: verum