theorem Th19: :: TOPMETR4:18

for NrSp being RealNormSpace
for S being Subset of NrSp
for T being Subset of (MetricSpaceNorm NrSp) st S = T holds
( S is compact iff T is sequentially_compact )