theorem :: NDIFF_1:5

for S being RealNormSpace
for X being Subset of S holds
( ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4;