theorem Th12: :: TOPMETR4:12

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