theorem :: TOPMETR4:10

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