for X being RealNormSpace
for A being Subset of X holds
( A is closed iff Cl A = A )