theorem OP1: :: NDIFF_8:26

for E being RealNormSpace
for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds
Y is open