for p, q being Point of (TOP-REAL 2)
for r being Real
for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )