theorem Th3: :: TOPMETR4:5

for M being non empty MetrSpace
for X being Subset of (TopSpaceMetr 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 ) )