let R be Subset of (TOP-REAL 2); :: thesis: for p, p1, p2 being Point of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let P be Subset of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let r be Real; :: thesis: for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let u be Point of (Euclid 2); :: thesis: ( p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R implies ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R ) )

assume that

A1: p <> p1 and

A2: P is_S-P_arc_joining p1,p2 and

A3: P c= R and

A4: p in Ball (u,r) and

A5: p2 in Ball (u,r) and

A6: Ball (u,r) c= R ; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

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

A7: f is being_S-Seq and

A8: P = L~ f and

A9: p1 = f /. 1 and

A10: p2 = f /. (len f) by A2;

( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum

for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let P be Subset of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let r be Real; :: thesis: for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

let u be Point of (Euclid 2); :: thesis: ( p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R implies ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R ) )

assume that

A1: p <> p1 and

A2: P is_S-P_arc_joining p1,p2 and

A3: P c= R and

A4: p in Ball (u,r) and

A5: p2 in Ball (u,r) and

A6: Ball (u,r) c= R ; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

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

A7: f is being_S-Seq and

A8: P = L~ f and

A9: p1 = f /. 1 and

A10: p2 = f /. (len f) by A2;

now :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )end;

hence
ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R )

per cases
( p1 in Ball (u,r) or not p1 in Ball (u,r) )
;

end;

suppose
p1 in Ball (u,r)
; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

( P1 is_S-P_arc_joining p1,p & P1 c= R )

then consider P1 being Subset of (TOP-REAL 2) such that

A11: ( P1 is_S-P_arc_joining p1,p & P1 c= Ball (u,r) ) by A1, A4, Th10;

reconsider P1 = P1 as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A6, A11; :: thesis: verum

end;A11: ( P1 is_S-P_arc_joining p1,p & P1 c= Ball (u,r) ) by A1, A4, Th10;

reconsider P1 = P1 as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A6, A11; :: thesis: verum

suppose A12:
not p1 in Ball (u,r)
; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum

end;

( P1 is_S-P_arc_joining p1,p & P1 c= R )

now :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )end;

hence
ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R )

per cases
( p in P or not p in P )
;

end;

suppose
p in P
; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

( P1 is_S-P_arc_joining p1,p & P1 c= R )

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

h is being_S-Seq and

h /. 1 = p1 and

h /. (len h) = p and

A13: ( L~ h is_S-P_arc_joining p1,p & L~ h c= L~ f ) by A1, A7, A8, A9, Th18;

reconsider P1 = L~ h as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A3, A8, A13; :: thesis: verum

end;h is being_S-Seq and

h /. 1 = p1 and

h /. (len h) = p and

A13: ( L~ h is_S-P_arc_joining p1,p & L~ h c= L~ f ) by A1, A7, A8, A9, Th18;

reconsider P1 = L~ h as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A3, A8, A13; :: thesis: verum

suppose
not p in P
; :: thesis: ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

( P1 is_S-P_arc_joining p1,p & P1 c= R )

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

A14: L~ h is_S-P_arc_joining p1,p and

A15: L~ h c= (L~ f) \/ (Ball (u,r)) by A4, A5, A7, A8, A9, A10, A12, Th22;

reconsider P1 = L~ h as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus P1 is_S-P_arc_joining p1,p by A14; :: thesis: P1 c= R

(L~ f) \/ (Ball (u,r)) c= R by A3, A6, A8, XBOOLE_1:8;

hence P1 c= R by A15; :: thesis: verum

end;A14: L~ h is_S-P_arc_joining p1,p and

A15: L~ h c= (L~ f) \/ (Ball (u,r)) by A4, A5, A7, A8, A9, A10, A12, Th22;

reconsider P1 = L~ h as Subset of (TOP-REAL 2) ;

take P1 = P1; :: thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R )

thus P1 is_S-P_arc_joining p1,p by A14; :: thesis: P1 c= R

(L~ f) \/ (Ball (u,r)) c= R by A3, A6, A8, XBOOLE_1:8;

hence P1 c= R by A15; :: thesis: verum

( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum

( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum