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