theorem :: NDIFF13:61

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