let R be Subset of (); :: thesis: for p, p1, p2 being Point of ()
for P being Subset of ()
for r being Real
for u being Point of () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

let p, p1, p2 be Point of (); :: thesis: for P being Subset of ()
for r being Real
for u being Point of () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

let P be Subset of (); :: thesis: for r being Real
for u being Point of () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

let r be Real; :: thesis: for u being Point of () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

let u be Point of (); :: 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 () 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 () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

consider f being FinSequence of () 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 () 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) ) ;
suppose p1 in Ball (u,r) ; :: thesis: ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

then consider P1 being Subset of () 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 () ;
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 ; :: thesis: verum
end;
suppose A12: not p1 in Ball (u,r) ; :: thesis: ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

now :: thesis: ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )
per cases ( p in P or not p in P ) ;
suppose p in P ; :: thesis: ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

then consider h being FinSequence of () 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 () ;
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;
suppose not p in P ; :: thesis: ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R )

then consider h being FinSequence of () 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 () ;
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 ;
hence P1 c= R by A15; :: thesis: verum
end;
end;
end;
hence ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum
end;
end;
end;
hence ex P1 being Subset of () st
( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; :: thesis: verum