theorem Th1: :: TOPMETR3:1

for X being non empty MetrSpace
for S being sequence of X
for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds
lim S in F