theorem :: NDIFF_8:23

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