for M being non empty MetrSpace st TopSpaceMetr M is countably_compact holds
M is sequentially_compact