theorem Th34: :: COMPL_SP:35

for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact )