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