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 S1[ 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 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 :: thesis: not (Ball (u,r)) /\ (L~ (f | m)) <> {}
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;
for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
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)) )
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
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 ) )
per cases ( p `1 = q `1 or p `2 = q `2 ) by A37;
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, A48, 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, A48, TOPREAL3:6; :: thesis: verum
end;
end;
end;
A50: (LSeg (q,p)) /\ (L~ h) c= {q}
proof
A51: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13;
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 A34, A16, A40, 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 A34, A16, A40, TOPREAL3:12; :: thesis: verum
end;
end;
end;
LSeg (q,p) = (LSeg (q,p)) /\ (Ball (u,r)) by A3, A38, TOPREAL3:21, XBOOLE_1:28;
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)
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;
let x be object ; :: 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, A33, A38, A49, A46, A52, A53, A51, TOPREAL3:42; :: thesis: verum
end;
q in L~ h by A44, Th3;
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;
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)) )
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;
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)) )
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;
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)) )
set v = |[(q `1),(p `2)]|;
A68: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) c= {q}
proof
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 ;
A71: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13;
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 A34, A16, A57, 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 A34, A16, A57, TOPREAL3:12; :: thesis: verum
end;
end;
end;
now :: thesis: x in {q}
per cases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A71;
suppose A72: q1 `1 = q `1 ; :: thesis: x in {q}
now :: thesis: not |[(q `1),(p `2)]| in LSeg (q1,q)
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;
hence x in {q} by A33, A65, A58, A64, A67, A70, A69, A72, 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 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;
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)) )
set v = |[(p `1),(q `2)]|;
A79: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) c= {q}
proof
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 ;
A82: now :: thesis: ( q1 `1 = q `1 or q1 `2 = q `2 )
per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13;
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 A34, A16, A57, 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 A34, A16, A57, TOPREAL3:12; :: thesis: verum
end;
end;
end;
now :: thesis: x in {q}
per cases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A82;
suppose A83: q1 `2 = q `2 ; :: thesis: x in {q}
now :: thesis: not |[(p `1),(q `2)]| in LSeg (q1,q)
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;
hence x in {q} by A33, A65, A58, A64, A78, A81, A80, A83, 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 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;
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