theorem :: TOPREAL3:22

for p, p1, p2 being Point of (TOP-REAL 2)
for r, r1, r2, s1, s2 being Real
for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds
p in Ball (u,r)