theorem :: NDIFF10:5

for X, Y being RealNormSpace
for V being Subset of [:X,Y:]
for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds
V is open