for p, q being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being Real st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )