theorem :: NORMSP_3:1

for X being RealNormSpace
for R being Subset of X holds
( R is closed iff R ` is open ) ;