theorem :: NORMSP_3:12

for X being RealNormSpace
for A being Subset of X holds
( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )