for M being non empty MetrSpace
for S being Subset of M
for T being Subset of (TopSpaceMetr M) st T = S holds
( T is compact iff S is sequentially_compact )