theorem :: TOPMETR4:14

for M being non empty MetrSpace
for S being non empty Subset of M holds
( S is sequentially_compact iff M | S is compact )