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 8;
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 8;
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 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 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
set x = the 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: 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 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: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;
now
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} implies m <= i )
assume that
A33: ( 1 <= i & i <= (len f) - 1 ) and
A34: (LSeg (f,i)) /\ (Ball (u,r)) <> {} ; :: thesis: m <= i
LSeg (f,i) meets Ball (u,r) by A34, XBOOLE_0:def 7;
hence m <= i by A11, A33; :: thesis: verum
end;
then A35: not q1 in Ball (u,r) by A1, A10, A12, TOPREAL3:26;
set A = (LSeg (f,m)) /\ (Ball (u,r));
A36: ( 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 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:74;
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:68;
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;
A51: now
per cases ( p `1 = q `1 or p `2 = q `2 ) by A39;
suppose p `1 = q `1 ; :: thesis: ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) )
hence ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) by A5, A50, TOPREAL3:6; :: thesis: verum
end;
suppose p `2 = q `2 ; :: thesis: ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) )
hence ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) by A5, A50, TOPREAL3:6; :: thesis: verum
end;
end;
end;
A52: (LSeg (q,p)) /\ (L~ h) c= {q}
proof
A53: now
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def 5;
suppose q1 `1 = q2 `1 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A42, TOPREAL3:11; :: thesis: verum
end;
suppose q1 `2 = q2 `2 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A42, TOPREAL3:12; :: thesis: verum
end;
end;
end;
LSeg (q,p) = (LSeg (q,p)) /\ (Ball (u,r)) by A3, A40, TOPREAL3:21, 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 ;
A55: now
q1 in LSeg (q1,q2) by RLTOPSP1:68;
then A56: LSeg (q1,q) c= LSeg (f,m) by A16, A42, TOPREAL1:6;
assume p in LSeg (q1,q) ; :: thesis: contradiction
hence contradiction by A5, A37, A56, TARSKI:def 3; :: thesis: verum
end;
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:42; :: 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:31;
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)) )
set x = the Element of (LSeg (f,m)) /\ (Ball (u,r));
A59: 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) ;
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:53;
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:25;
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: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 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 ;
A73: now
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def 5;
suppose q1 `1 = q2 `1 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:11; :: thesis: verum
end;
suppose q1 `2 = q2 `2 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:12; :: thesis: verum
end;
end;
end;
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:68;
then A75: LSeg (q1,q) c= LSeg (f,m) by A16, A59, TOPREAL1:6;
A76: |[(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 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:43; :: thesis: verum
end;
end;
end;
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:68;
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:31;
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: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 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 ;
A84: now
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def 5;
suppose q1 `1 = q2 `1 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:11; :: thesis: verum
end;
suppose q1 `2 = q2 `2 ; :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:12; :: thesis: verum
end;
end;
end;
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:68;
then A86: LSeg (q1,q) c= LSeg (f,m) by A16, A59, TOPREAL1:6;
A87: |[(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 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:44; :: thesis: verum
end;
end;
end;
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:68;
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:31;
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;
end;
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;
end;
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