theorem :: COMPL_SP:37

for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff ( M is totally_bounded & M is complete ) )