for T being NormedLinearTopSpace
for X being set holds
( X is compact Subset of T iff X is compact Subset of (TopSpaceNorm T) )