theorem Th23: :: TOPREAL4:23

for R being Subset of (TOP-REAL 2)
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 )