theorem Th16: :: TOPMETR4:15

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 )