let M be non empty MetrSpace; :: thesis: ( ( M is totally_bounded & M is complete ) iff M is sequentially_compact )
( ( M is totally_bounded & M is complete ) iff TopSpaceMetr M is compact ) by COMPL_SP:37;
hence ( ( M is totally_bounded & M is complete ) iff M is sequentially_compact ) by Th11; :: thesis: verum