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