theorem :: TOPMETR4:19

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