for p being Point of (TOP-REAL 2) st p `2 = 0 holds
for x being Real
for r being positive Real st (+ (x,r)) . p = 1 holds
ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}