theorem Th28: :: FRECHET2:28

for M being non empty MetrSpace
for S being sequence of M
for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )