theorem :: RUSUB_7:7

for X being RealUnitarySpace
for V being Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )