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 & P = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A2, Def1;

now

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

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 )

then consider P1 being Subset of (TOP-REAL 2) such that
A8: ( P1 is_S-P_arc_joining p1,p & P1 c= Ball u,r ) by A1, A4, Th11;
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, A8, XBOOLE_1:1; :: thesis: verum

end;

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

now

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

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 )

then consider h being FinSequence of (TOP-REAL 2) such that
A10: ( h is being_S-Seq & h /. 1 = p1 & h /. (len h) = p & L~ h is_S-P_arc_joining p1,p & L~ h c= L~ f ) by A1, A7, Th19;
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, A7, A10, XBOOLE_1:1; :: thesis: verum

end;

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 )

then consider h being FinSequence of (TOP-REAL 2) such that
A11: ( L~ h is_S-P_arc_joining p1,p & L~ h c= (L~ f) \/ (Ball u,r) ) by A4, A5, A7, A9, Th23;
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 A11; :: thesis: P1 c= R
(L~ f) \/ (Ball u,r) c= R by A3, A6, A7, XBOOLE_1:8;
hence P1 c= R by A11, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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