for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
ex x being Element of X st S is_convergent_in_metrspace_to x