for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )