theorem Th7: :: METRIC_6:7

for X being non empty MetrSpace
for x being Element of X ex S being sequence of X st rng S = {x}