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 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;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= (len f) - 1 & LSeg (f,$1) meets Ball (u,r) );

A7: len f >= 2 by A4;

then reconsider n = (len f) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;

2 = 1 + 1 ;

then A8: 1 <= (len f) - 1 by A7, XREAL_1:19;

n + 1 = len f ;

then f /. (len f) in LSeg (f,n) by A8, TOPREAL1:21;

then LSeg (f,n) meets Ball (u,r) by A2, XBOOLE_0:3;

then A9: ex n being Nat st S_{1}[n]
by A8;

consider m being Nat such that

A10: S_{1}[m]
and

A11: for i being Nat st S_{1}[i] holds

m <= i from NAT_1:sch 5(A9);

reconsider m = m as Element of NAT by ORDINAL1:def 12;

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:19;

then A16: LSeg (f,m) = LSeg (q1,q2) by A10, A12, A13, TOPREAL1:def 3;

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;

m <= i by A11, XBOOLE_0:def 7;

then A33: not q1 in Ball (u,r) by A1, A10, A12, TOPREAL3:26;

set A = (LSeg (f,m)) /\ (Ball (u,r));

A34: ( q1 = |[(q1 `1),(q1 `2)]| & q2 = |[(q2 `1),(q2 `2)]| ) by EUCLID:53;

m + 1 <= n + 1 by A10, XREAL_1:6;

then LSeg (f,m) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A10;

then A35: LSeg (f,m) c= union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by ZFMISC_1:74;

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ; :: thesis: verum

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 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;

defpred S

A7: len f >= 2 by A4;

then reconsider n = (len f) - 1 as Element of NAT by INT_1:5, XXREAL_0:2;

2 = 1 + 1 ;

then A8: 1 <= (len f) - 1 by A7, XREAL_1:19;

n + 1 = len f ;

then f /. (len f) in LSeg (f,n) by A8, TOPREAL1:21;

then LSeg (f,n) meets Ball (u,r) by A2, XBOOLE_0:3;

then A9: ex n being Nat st S

consider m being Nat such that

A10: S

A11: for i being Nat st S

m <= i from NAT_1:sch 5(A9);

reconsider m = m as Element of NAT by ORDINAL1:def 12;

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:19;

then A16: LSeg (f,m) = LSeg (q1,q2) by A10, A12, A13, TOPREAL1:def 3;

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 :: thesis: not (Ball (u,r)) /\ (L~ (f | m)) <> {}

for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds set x = the Element of (Ball (u,r)) /\ (L~ (f | m));

set M = { (LSeg ((f | m),i)) where i is 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: contradiction

then A22: the Element of (Ball (u,r)) /\ (L~ (f | m)) in Ball (u,r) by XBOOLE_0:def 4;

the Element of (Ball (u,r)) /\ (L~ (f | m)) in L~ (f | m) by A21, XBOOLE_0:def 4;

then consider X being set such that

A23: the Element of (Ball (u,r)) /\ (L~ (f | m)) in X and

A24: X in { (LSeg ((f | m),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f | m) ) } by TARSKI:def 4;

consider k being 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:1;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len (f | m)) by A27, FINSEQ_1:1;

then the Element of (Ball (u,r)) /\ (L~ (f | m)) in LSeg (f,k) by A23, A25, A28, A20, TOPREAL3:17;

then A29: LSeg (f,k) meets Ball (u,r) by A22, XBOOLE_0:3;

Seg m c= Seg (len f) by A17, FINSEQ_1:5;

then A30: Seg m = (dom f) /\ (Seg m) by A18, XBOOLE_1:28

.= dom (f | (Seg m)) by RELAT_1:61

.= Seg (len (f | m)) by A20, FINSEQ_1:def 15 ;

A31: (k + 1) - 1 <= (len (f | m)) - 1 by A27, XREAL_1:9;

then A32: k <= m - 1 by A30, FINSEQ_1:6;

m = len (f | m) by A30, FINSEQ_1:6;

then (len (f | m)) - 1 <= (len f) - 1 by A17, XREAL_1:9;

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:48;

hence contradiction ; :: thesis: verum

end;set M = { (LSeg ((f | m),i)) where i is 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: contradiction

then A22: the Element of (Ball (u,r)) /\ (L~ (f | m)) in Ball (u,r) by XBOOLE_0:def 4;

the Element of (Ball (u,r)) /\ (L~ (f | m)) in L~ (f | m) by A21, XBOOLE_0:def 4;

then consider X being set such that

A23: the Element of (Ball (u,r)) /\ (L~ (f | m)) in X and

A24: X in { (LSeg ((f | m),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f | m) ) } by TARSKI:def 4;

consider k being 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:1;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len (f | m)) by A27, FINSEQ_1:1;

then the Element of (Ball (u,r)) /\ (L~ (f | m)) in LSeg (f,k) by A23, A25, A28, A20, TOPREAL3:17;

then A29: LSeg (f,k) meets Ball (u,r) by A22, XBOOLE_0:3;

Seg m c= Seg (len f) by A17, FINSEQ_1:5;

then A30: Seg m = (dom f) /\ (Seg m) by A18, XBOOLE_1:28

.= dom (f | (Seg m)) by RELAT_1:61

.= Seg (len (f | m)) by A20, FINSEQ_1:def 15 ;

A31: (k + 1) - 1 <= (len (f | m)) - 1 by A27, XREAL_1:9;

then A32: k <= m - 1 by A30, FINSEQ_1:6;

m = len (f | m) by A30, FINSEQ_1:6;

then (len (f | m)) - 1 <= (len f) - 1 by A17, XREAL_1:9;

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:48;

hence contradiction ; :: thesis: verum

m <= i by A11, XBOOLE_0:def 7;

then A33: not q1 in Ball (u,r) by A1, A10, A12, TOPREAL3:26;

set A = (LSeg (f,m)) /\ (Ball (u,r));

A34: ( q1 = |[(q1 `1),(q1 `2)]| & q2 = |[(q2 `1),(q2 `2)]| ) by EUCLID:53;

m + 1 <= n + 1 by A10, XREAL_1:6;

then LSeg (f,m) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A10;

then A35: LSeg (f,m) c= union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by ZFMISC_1:74;

now :: 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)) )end;

hence
ex h being FinSequence of (TOP-REAL 2) st ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

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 ) ) ;

end;

( 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)) )

( 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

A36: q in (LSeg (f,m)) /\ (Ball (u,r)) and

A37: ( p `1 = q `1 or p `2 = q `2 ) ;

A38: q in Ball (u,r) by A36, XBOOLE_0:def 4;

A39: q in LSeg (q,p) by RLTOPSP1:68;

A40: q in LSeg (f,m) by A36, XBOOLE_0:def 4;

then consider h being FinSequence of (TOP-REAL 2) such that

A41: h is being_S-Seq and

A42: h /. 1 = f /. 1 and

A43: h /. (len h) = q and

A44: L~ h is_S-P_arc_joining f /. 1,q and

A45: L~ h c= L~ f and

A46: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A1, A4, A12, A38, Th17;

take g = h ^ <*p*>; :: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

A47: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A45, XBOOLE_1:9;

A48: q in L~ f by A35, A40;

then q in (LSeg (q,p)) /\ (L~ h) by A39, XBOOLE_0:def 4;

then {q} c= (LSeg (q,p)) /\ (L~ h) by ZFMISC_1:31;

then A55: (LSeg (q,p)) /\ (L~ h) = {q} by A50;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A38, A49, A41, A43, Th19;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A38, A49, A41, A42, A43, A55, A47, Th19; :: thesis: verum

end;A36: q in (LSeg (f,m)) /\ (Ball (u,r)) and

A37: ( p `1 = q `1 or p `2 = q `2 ) ;

A38: q in Ball (u,r) by A36, XBOOLE_0:def 4;

A39: q in LSeg (q,p) by RLTOPSP1:68;

A40: q in LSeg (f,m) by A36, XBOOLE_0:def 4;

then consider h being FinSequence of (TOP-REAL 2) such that

A41: h is being_S-Seq and

A42: h /. 1 = f /. 1 and

A43: h /. (len h) = q and

A44: L~ h is_S-P_arc_joining f /. 1,q and

A45: L~ h c= L~ f and

A46: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A1, A4, A12, A38, Th17;

take g = h ^ <*p*>; :: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

A47: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A45, XBOOLE_1:9;

A48: q in L~ f by A35, A40;

A49: now :: thesis: ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) )

A50:
(LSeg (q,p)) /\ (L~ h) c= {q}
end;

proof

then A52: (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 ;

assume x in (LSeg (q,p)) /\ (L~ h) ; :: thesis: x in {q}

hence x in {q} by A3, A33, A38, A49, A46, A52, A53, A51, TOPREAL3:42; :: thesis: verum

end;

q in L~ h
by A44, Th3;A51: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )

LSeg (q,p) = (LSeg (q,p)) /\ (Ball (u,r))
by A3, A38, TOPREAL3:21, XBOOLE_1:28;end;

then A52: (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 ;

A53: now :: thesis: not p in LSeg (q1,q)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (q,p)) /\ (L~ h) or x in {q} )
q1 in LSeg (q1,q2)
by RLTOPSP1:68;

then A54: LSeg (q1,q) c= LSeg (f,m) by A16, A40, TOPREAL1:6;

assume p in LSeg (q1,q) ; :: thesis: contradiction

hence contradiction by A5, A35, A54; :: thesis: verum

end;then A54: LSeg (q1,q) c= LSeg (f,m) by A16, A40, TOPREAL1:6;

assume p in LSeg (q1,q) ; :: thesis: contradiction

hence contradiction by A5, A35, A54; :: thesis: verum

assume x in (LSeg (q,p)) /\ (L~ h) ; :: thesis: x in {q}

hence x in {q} by A3, A33, A38, A49, A46, A52, A53, A51, TOPREAL3:42; :: thesis: verum

then q in (LSeg (q,p)) /\ (L~ h) by A39, XBOOLE_0:def 4;

then {q} c= (LSeg (q,p)) /\ (L~ h) by ZFMISC_1:31;

then A55: (LSeg (q,p)) /\ (L~ h) = {q} by A50;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A38, A49, A41, A43, Th19;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A38, A49, A41, A42, A43, A55, A47, Th19; :: thesis: verum

suppose A56:
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)) )

( 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)) )

set x = the Element of (LSeg (f,m)) /\ (Ball (u,r));

A57: the Element of (LSeg (f,m)) /\ (Ball (u,r)) in LSeg (f,m) by A14, XBOOLE_0:def 4;

then reconsider q = the Element of (LSeg (f,m)) /\ (Ball (u,r)) as Point of (TOP-REAL 2) ;

A58: ( q `1 <> p `1 & q `2 <> p `2 ) by A14, A56;

q <> f /. 1 by A1, A14, XBOOLE_0:def 4;

then consider h being FinSequence of (TOP-REAL 2) such that

A59: h is being_S-Seq and

A60: h /. 1 = f /. 1 and

A61: h /. (len h) = q and

A62: L~ h is_S-P_arc_joining f /. 1,q and

A63: L~ h c= L~ f and

A64: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A4, A12, A57, Th17;

A65: q in Ball (u,r) by A14, XBOOLE_0:def 4;

A66: ( q = |[(q `1),(q `2)]| & p = |[(p `1),(p `2)]| ) by EUCLID:53;

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ; :: thesis: verum

end;A57: the Element of (LSeg (f,m)) /\ (Ball (u,r)) in LSeg (f,m) by A14, XBOOLE_0:def 4;

then reconsider q = the Element of (LSeg (f,m)) /\ (Ball (u,r)) as Point of (TOP-REAL 2) ;

A58: ( q `1 <> p `1 & q `2 <> p `2 ) by A14, A56;

q <> f /. 1 by A1, A14, XBOOLE_0:def 4;

then consider h being FinSequence of (TOP-REAL 2) such that

A59: h is being_S-Seq and

A60: h /. 1 = f /. 1 and

A61: h /. (len h) = q and

A62: L~ h is_S-P_arc_joining f /. 1,q and

A63: L~ h c= L~ f and

A64: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A4, A12, A57, Th17;

A65: q in Ball (u,r) by A14, XBOOLE_0:def 4;

A66: ( q = |[(q `1),(q `2)]| & p = |[(p `1),(p `2)]| ) by EUCLID:53;

now :: 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)) )end;

hence
ex h being FinSequence of (TOP-REAL 2) st ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

per cases
( |[(q `1),(p `2)]| in Ball (u,r) or |[(p `1),(q `2)]| in Ball (u,r) )
by A3, A65, A66, TOPREAL3:25;

end;

suppose A67:
|[(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)) )

( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

set v = |[(q `1),(p `2)]|;

A68: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) c= {q}

q in LSeg (q,|[(q `1),(p `2)]|) by RLTOPSP1:68;

then A75: q in (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p)) by XBOOLE_0:def 3;

A76: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A63, XBOOLE_1:9;

q in L~ h by A62, Th3;

then q in ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by A75, XBOOLE_0:def 4;

then {q} c= ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by ZFMISC_1:31;

then A77: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) = {q} by A68;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A65, A58, A59, A61, A67, Th21;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A65, A58, A59, A60, A61, A67, A77, A76, Th21; :: thesis: verum

end;A68: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) c= {q}

proof

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)) )
let x be object ; :: 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 A69: 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, A65, A67, TOPREAL3:21;

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 A70: ((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 ;

end;set L = (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p));

assume A69: 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, A65, A67, TOPREAL3:21;

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 A70: ((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 ;

A71: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )

end;

now :: thesis: x in {q}end;

hence
x in {q}
; :: thesis: verumper cases
( q1 `1 = q `1 or q1 `2 = q `2 )
by A71;

end;

suppose A72:
q1 `1 = q `1
; :: thesis: x in {q}

end;

now :: thesis: not |[(q `1),(p `2)]| in LSeg (q1,q)

hence
x in {q}
by A33, A65, A58, A64, A67, A70, A69, A72, TOPREAL3:43; :: thesis: verum
q1 in LSeg (q1,q2)
by RLTOPSP1:68;

then A73: LSeg (q1,q) c= LSeg (f,m) by A16, A57, TOPREAL1:6;

A74: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52;

assume |[(q `1),(p `2)]| in LSeg (q1,q) ; :: thesis: contradiction

then |[(q `1),(p `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A67, A73, XBOOLE_0:def 4;

hence contradiction by A56, A74; :: thesis: verum

end;then A73: LSeg (q1,q) c= LSeg (f,m) by A16, A57, TOPREAL1:6;

A74: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52;

assume |[(q `1),(p `2)]| in LSeg (q1,q) ; :: thesis: contradiction

then |[(q `1),(p `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A67, A73, XBOOLE_0:def 4;

hence contradiction by A56, A74; :: thesis: verum

q in LSeg (q,|[(q `1),(p `2)]|) by RLTOPSP1:68;

then A75: q in (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p)) by XBOOLE_0:def 3;

A76: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A63, XBOOLE_1:9;

q in L~ h by A62, Th3;

then q in ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by A75, XBOOLE_0:def 4;

then {q} c= ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by ZFMISC_1:31;

then A77: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) = {q} by A68;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A65, A58, A59, A61, A67, Th21;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A65, A58, A59, A60, A61, A67, A77, A76, Th21; :: thesis: verum

suppose A78:
|[(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)) )

( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) )

set v = |[(p `1),(q `2)]|;

A79: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) c= {q}

q in LSeg (q,|[(p `1),(q `2)]|) by RLTOPSP1:68;

then A86: q in (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p)) by XBOOLE_0:def 3;

A87: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A63, XBOOLE_1:9;

q in L~ h by A62, Th3;

then q in ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by A86, XBOOLE_0:def 4;

then {q} c= ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by ZFMISC_1:31;

then A88: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) = {q} by A79;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A65, A58, A59, A61, A78, Th20;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A65, A58, A59, A60, A61, A78, A88, A87, Th20; :: thesis: verum

end;A79: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) c= {q}

proof

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)) )
let x be object ; :: 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 A80: 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, A65, A78, TOPREAL3:21;

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 A81: ((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 ;

end;set L = (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p));

assume A80: 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, A65, A78, TOPREAL3:21;

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 A81: ((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 ;

A82: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )

end;

now :: thesis: x in {q}end;

hence
x in {q}
; :: thesis: verumper cases
( q1 `1 = q `1 or q1 `2 = q `2 )
by A82;

end;

suppose A83:
q1 `2 = q `2
; :: thesis: x in {q}

end;

now :: thesis: not |[(p `1),(q `2)]| in LSeg (q1,q)

hence
x in {q}
by A33, A65, A58, A64, A78, A81, A80, A83, TOPREAL3:44; :: thesis: verum
q1 in LSeg (q1,q2)
by RLTOPSP1:68;

then A84: LSeg (q1,q) c= LSeg (f,m) by A16, A57, TOPREAL1:6;

A85: |[(p `1),(q `2)]| `1 = p `1 by EUCLID:52;

assume |[(p `1),(q `2)]| in LSeg (q1,q) ; :: thesis: contradiction

then |[(p `1),(q `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A78, A84, XBOOLE_0:def 4;

hence contradiction by A56, A85; :: thesis: verum

end;then A84: LSeg (q1,q) c= LSeg (f,m) by A16, A57, TOPREAL1:6;

A85: |[(p `1),(q `2)]| `1 = p `1 by EUCLID:52;

assume |[(p `1),(q `2)]| in LSeg (q1,q) ; :: thesis: contradiction

then |[(p `1),(q `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A78, A84, XBOOLE_0:def 4;

hence contradiction by A56, A85; :: thesis: verum

q in LSeg (q,|[(p `1),(q `2)]|) by RLTOPSP1:68;

then A86: q in (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p)) by XBOOLE_0:def 3;

A87: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A63, XBOOLE_1:9;

q in L~ h by A62, Th3;

then q in ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by A86, XBOOLE_0:def 4;

then {q} c= ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by ZFMISC_1:31;

then A88: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) = {q} by A79;

then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A65, A58, A59, A61, A78, Th20;

hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A65, A58, A59, A60, A61, A78, A88, A87, Th20; :: thesis: verum

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ; :: thesis: verum

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ; :: thesis: verum