for X being RealNormSpace
for Y being Subset of X
for v being object holds
( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )