for p being Point of (TOP-REAL 2) st p `2 >= 0 holds
for x, a, b being Real
for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )