for X being RealNormSpace
for Y being Subset of X
for v being object st v in the carrier of X holds
( v in Cl Y iff for G being Subset of X st G is open & v in G holds
G meets Y )