for S being RealNormSpace
for X being Subset of S st ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open