theorem Th40: :: TOPREAL6:42

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