theorem Th11: :: METRIC_6:11

for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x