theorem Th4: :: NDIFF10:4

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