let M be non empty MetrSpace; :: thesis: ( TopSpaceMetr M is compact iff M is sequentially_compact )
thus ( TopSpaceMetr M is compact implies M is sequentially_compact ) by Th8, COMPL_SP:35; :: thesis: ( M is sequentially_compact implies TopSpaceMetr M is compact )
assume M is sequentially_compact ; :: thesis: TopSpaceMetr M is compact
then ( M is totally_bounded & M is complete ) by Th10;
hence TopSpaceMetr M is compact by COMPL_SP:37; :: thesis: verum