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