let R be Subset of (TOP-REAL 2); :: thesis:
let p, p1, p2 be Point of (TOP-REAL 2); :: thesis:
let P be Subset of (TOP-REAL 2); :: thesis:
let r be Real; :: thesis:
let u be Point of (Euclid 2); :: thesis:
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:
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;

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:
thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A6, A11; :: thesis:

end;

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:
thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A3, A8, A13; :: thesis:

end;

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:
thus P1 is_S-P_arc_joining p1,p by A14; :: thesis:
(L~ f) \/ (Ball (u,r)) c= R by A3, A6, A8, XBOOLE_1:8;
hence P1 c= R by A15; :: thesis:

end;

end;