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 A1: ( 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 ) ; :: 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) )
then ( len f >= 2 & 2 = 1 + 1 ) by TOPREAL1:def 10;
then A2: ( len f >= 1 & 1 <= (len f) - 1 ) by XREAL_1:21, XXREAL_0:2;
then reconsider n = (len f) - 1 as Element of NAT by INT_1:18;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= (len f) - 1 & LSeg f,$1 meets Ball u,r );
A3: f is special by A1, TOPREAL1:def 10;
n + 1 = len f ;
then f /. (len f) in LSeg f,n by A2, TOPREAL1:27;
then LSeg f,n meets Ball u,r by A1, XBOOLE_0:3;
then A4: ex n being Nat st S₁[n] by A2;
consider m being Nat such that
A5: S₁[m] and
A6: for i being Nat st S₁[i] holds
m <= i from NAT_1:sch 5(A4);
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A7: (LSeg f,m) /\ (Ball u,r) <> {} by A5, XBOOLE_0:def 7;

A8: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (len f) - 1 & (LSeg f,i) /\ (Ball u,r) <> {} implies m <= i )
assume ( 1 <= i & i <= (len f) - 1 & (LSeg f,i) /\ (Ball u,r) <> {} ) ; :: thesis: m <= i
then ( 1 <= i & i <= (len f) - 1 & LSeg f,i meets Ball u,r ) by XBOOLE_0:def 7;
hence m <= i by A6; :: thesis: verum

end;

m + 1 <= n + 1 by A5, XREAL_1:8;
then LSeg f,m in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A5;
then A9: LSeg f,m c= union { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by ZFMISC_1:92;
set A = (LSeg f,m) /\ (Ball u,r);
A10: ( m + 1 <= len f & m <= m + 1 ) by A5, NAT_1:11, XREAL_1:21;
then A11: ( 1 <= m & m <= len f & m + 1 <= len f ) by A5, XXREAL_0:2;
then A12: ( m in Seg (len f) & Seg (len f) = dom f ) by FINSEQ_1:3, FINSEQ_1:def 3;
consider q1, q2 being Point of (TOP-REAL 2) such that
A13: ( f /. m = q1 & f /. (m + 1) = q2 ) ;
A14: not q1 in Ball u,r by A1, A5, A8, A13, TOPREAL3:33;

A15: now

set M = { (LSeg (f | m),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | m) ) } ;
assume A16: (Ball u,r) /\ (L~ (f | m)) <> {} ; :: thesis: contradiction
consider x being Element of (Ball u,r) /\ (L~ (f | m));
A17: ( x in L~ (f | m) & x in Ball u,r ) by A16, XBOOLE_0:def 4;
then consider X being set such that
A18: ( x in X & 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
A19: ( X = LSeg (f | m),k & 1 <= k & k + 1 <= len (f | m) ) by A18;
A20: (k + 1) - 1 <= (len (f | m)) - 1 by A19, XREAL_1:11;
k <= k + 1 by NAT_1:11;
then ( 1 <= k & k <= len (f | m) & 1 <= k + 1 & k + 1 <= len (f | m) ) by A19, XXREAL_0:2;
then A21: ( k in Seg (len (f | m)) & k + 1 in Seg (len (f | m)) & Seg (len (f | m)) = dom (f | m) ) by FINSEQ_1:3, FINSEQ_1:def 3;
then x in LSeg f,k by A12, A18, A19, TOPREAL3:24;
then A22: LSeg f,k meets Ball u,r by A17, XBOOLE_0:3;
Seg m c= Seg (len f) by A11, FINSEQ_1:7;
then A23: Seg m = (dom f) /\ (Seg m) by A12, XBOOLE_1:28
.= dom (f | (Seg m)) by RELAT_1:90
.= Seg (len (f | m)) by A21, FINSEQ_1:def 15 ;
then m = len (f | m) by FINSEQ_1:8;
then (len (f | m)) - 1 <= (len f) - 1 by A11, XREAL_1:11;
then k <= (len f) - 1 by A20, XXREAL_0:2;
then ( m <= k & k <= m - 1 ) by A6, A19, A20, A22, A23, FINSEQ_1:8;
then m <= m - 1 by XXREAL_0:2;
then 0 <= (m + (- 1)) - m by XREAL_1:50;
hence contradiction ; :: thesis: verum

end;

A24: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q2 = |[(q2 `1 ),(q2 `2 )]| ) by EUCLID:57;
A25: LSeg f,m = LSeg q1,q2 by A5, A10, A13, TOPREAL1:def 5;

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
A26: q in (LSeg f,m) /\ (Ball u,r) and
A27: ( p `1 = q `1 or p `2 = q `2 ) ;
A28: ( q in LSeg f,m & q in Ball u,r ) by A26, XBOOLE_0:def 4;
then A29: q in L~ f by A9;

A30: now

per cases ( p `1 = q `1 or p `2 = q `2 ) by A27;

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 A1, A29, TOPREAL3:11; :: 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 A1, A29, TOPREAL3:11; :: thesis: verum

end;

end;

end;

consider h being FinSequence of (TOP-REAL 2) such that
A31: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = q & L~ h is_S-P_arc_joining f /. 1,q & L~ h c= L~ f & L~ h = (L~ (f | m)) \/ (LSeg q1,q) ) by A1, A13, A28, Th18;
take g = h ^ <*p*>; :: thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) )
( q in L~ h & q in LSeg q,p ) by A31, Th4, RLTOPSP1:69;
then q in (LSeg q,p) /\ (L~ h) by XBOOLE_0:def 4;
then A32: {q} c= (LSeg q,p) /\ (L~ h) by ZFMISC_1:37;
(LSeg q,p) /\ (L~ h) c= {q}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg q,p) /\ (L~ h) or x in {q} )
assume A33: x in (LSeg q,p) /\ (L~ h) ; :: thesis: x in {q}
LSeg q,p = (LSeg q,p) /\ (Ball u,r) by A1, A28, TOPREAL3:28, XBOOLE_1:28;
then A34: (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 A15 ;

A35: now

( q1 in LSeg q1,q2 & q in LSeg q1,q2 ) by A5, A10, A13, A28, RLTOPSP1:69, TOPREAL1:def 5;
then A36: LSeg q1,q c= LSeg f,m by A25, TOPREAL1:12;
assume p in LSeg q1,q ; :: thesis: contradiction
hence contradiction by A1, A9, A36, TARSKI:def 3; :: thesis: verum

end;

now

per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A3, A5, A10, A13, TOPREAL1:def 7;

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 A24, A25, A28, TOPREAL3:17; :: 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 A24, A25, A28, TOPREAL3:18; :: thesis: verum

end;

end;

end;

hence x in {q} by A1, A14, A28, A30, A31, A33, A34, A35, TOPREAL3:49; :: thesis: verum

end;

then (LSeg q,p) /\ (L~ h) = {q} by A32, XBOOLE_0:def 10;
then A37: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ h) \/ (Ball u,r) ) by A1, A28, A30, A31, Th20;
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r) by A31, XBOOLE_1:9;
hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) ) by A37, XBOOLE_1:1; :: thesis: verum

end;

suppose A38: 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);
A39: ( x in LSeg f,m & LSeg f,m c= the carrier of (TOP-REAL 2) ) by A7, XBOOLE_0:def 4;
then reconsider q = x as Point of (TOP-REAL 2) ;
A40: ( q in Ball u,r & q `1 <> p `1 & q `2 <> p `2 & q = |[(q `1 ),(q `2 )]| & p = |[(p `1 ),(p `2 )]| ) by A7, A38, EUCLID:57, XBOOLE_0:def 4;
q <> f /. 1 by A1, A7, XBOOLE_0:def 4;
then consider h being FinSequence of (TOP-REAL 2) such that
A41: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = q & L~ h is_S-P_arc_joining f /. 1,q & L~ h c= L~ f & L~ h = (L~ (f | m)) \/ (LSeg q1,q) ) by A1, A13, A39, Th18;

now

per cases ( |[(q `1 ),(p `2 )]| in Ball u,r or |[(p `1 ),(q `2 )]| in Ball u,r ) by A1, A40, TOPREAL3:32;

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

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) )
set v = |[(q `1 ),(p `2 )]|;
( q in LSeg q,|[(q `1 ),(p `2 )]| & q in L~ h ) by A41, Th4, RLTOPSP1:69;
then ( q in (LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p) & q in L~ h ) by XBOOLE_0:def 3;
then q in ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) by XBOOLE_0:def 4;
then A43: {q} c= ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) by ZFMISC_1:37;
((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) c= {q}

proof

set L = (LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p);
( LSeg q,|[(q `1 ),(p `2 )]| c= Ball u,r & LSeg |[(q `1 ),(p `2 )]|,p c= Ball u,r ) by A1, A40, A42, 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 A44: ((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 A15 ;
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} )
assume A45: x in ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) ; :: thesis: x in {q}

A46: now

per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A3, A5, A10, A13, TOPREAL1:def 7;

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 A24, A25, A39, TOPREAL3:17; :: 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 A24, A25, A39, TOPREAL3:18; :: thesis: verum

end;

end;

end;

now

per cases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A46;

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

now

( q1 in LSeg q1,q2 & q in LSeg q1,q2 ) by A5, A10, A13, A39, RLTOPSP1:69, TOPREAL1:def 5;
then A48: LSeg q1,q c= LSeg f,m by A25, TOPREAL1:12;
assume |[(q `1 ),(p `2 )]| in LSeg q1,q ; :: thesis: contradiction
then ( |[(q `1 ),(p `2 )]| in (LSeg f,m) /\ (Ball u,r) & |[(q `1 ),(p `2 )]| `2 = p `2 ) by A42, A48, EUCLID:56, XBOOLE_0:def 4;
hence contradiction by A38; :: thesis: verum

end;

hence x in {q} by A1, A14, A40, A41, A42, A44, A45, A47, TOPREAL3:50; :: thesis: verum

end;

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

hence x in {q} by A40, A41, A44, A45, TOPREAL3:34; :: thesis: verum

end;

end;

end;

hence x in {q} ; :: thesis: verum

end;

then ((LSeg q,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,p)) /\ (L~ h) = {q} by A43, XBOOLE_0:def 10;
then A49: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ h) \/ (Ball u,r) ) by A1, A40, A41, A42, Th22;
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r) by A41, XBOOLE_1:9;
hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) ) by A49, XBOOLE_1:1; :: thesis: verum

end;

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

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) )
set v = |[(p `1 ),(q `2 )]|;
( q in LSeg q,|[(p `1 ),(q `2 )]| & q in L~ h ) by A41, Th4, RLTOPSP1:69;
then ( q in (LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p) & q in L~ h ) by XBOOLE_0:def 3;
then q in ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) by XBOOLE_0:def 4;
then A51: {q} c= ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) by ZFMISC_1:37;
((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) c= {q}

proof

set L = (LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p);
( LSeg q,|[(p `1 ),(q `2 )]| c= Ball u,r & LSeg |[(p `1 ),(q `2 )]|,p c= Ball u,r ) by A1, A40, A50, 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 A52: ((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 A15 ;
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} )
assume A53: x in ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) ; :: thesis: x in {q}

A54: now

per cases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A3, A5, A10, A13, TOPREAL1:def 7;

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 A24, A25, A39, TOPREAL3:17; :: 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 A24, A25, A39, TOPREAL3:18; :: thesis: verum

end;

end;

end;

now

per cases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A54;

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

hence x in {q} by A40, A41, A52, A53, TOPREAL3:35; :: thesis: verum

end;

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

now

( q1 in LSeg q1,q2 & q in LSeg q1,q2 ) by A5, A10, A13, A39, RLTOPSP1:69, TOPREAL1:def 5;
then A56: LSeg q1,q c= LSeg f,m by A25, TOPREAL1:12;
assume |[(p `1 ),(q `2 )]| in LSeg q1,q ; :: thesis: contradiction
then ( |[(p `1 ),(q `2 )]| in (LSeg f,m) /\ (Ball u,r) & |[(p `1 ),(q `2 )]| `1 = p `1 ) by A50, A56, EUCLID:56, XBOOLE_0:def 4;
hence contradiction by A38; :: thesis: verum

end;

hence x in {q} by A1, A14, A40, A41, A50, A52, A53, A55, TOPREAL3:51; :: thesis: verum

end;

end;

end;

hence x in {q} ; :: thesis: verum

end;

then ((LSeg q,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,p)) /\ (L~ h) = {q} by A51, XBOOLE_0:def 10;
then A57: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ h) \/ (Ball u,r) ) by A1, A40, A41, A50, Th21;
(L~ h) \/ (Ball u,r) c= (L~ f) \/ (Ball u,r) by A41, XBOOLE_1:9;
hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball u,r) ) by A57, 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