for a being Real
for f being Point of (Euclid 2)
for x being Point of (TOP-REAL 2) st x in Ball (f,a) holds
not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)