theorem :: NDIFF_8:24

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open