theorem NORMSP27: :: NDIFF_8:20

for X being RealNormSpace
for V being Subset of X holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )