for X being RealUnitarySpace
for Y being Subset of X holds
( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )