for M being non empty MetrSpace holds TopSpaceMetr M is first-countable