for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being Real st p = e holds
product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r)