theorem Th8: :: TOPMETR4:9

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