theorem Th10: :: RUSUB_7:10
for M being RealUnitarySpace
for X being Subset of (TopSpaceNorm (RUSp2RNSp M))
for x being object holds
( x in Cl X iff ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )