let NrSp be RealNormSpace; :: thesis: for S being Subset of NrSp
for T being Subset of (TopSpaceNorm NrSp) st S = T holds
( S is compact iff T is compact )
let S be Subset of NrSp; :: thesis: for T being Subset of (TopSpaceNorm NrSp) st S = T holds
( S is compact iff T is compact )
let T be Subset of (TopSpaceNorm NrSp); :: thesis: ( S = T implies ( S is compact iff T is compact ) )
assume A1: S = T ; :: thesis: ( S is compact iff T is compact )
reconsider W = S as Subset of (MetricSpaceNorm NrSp) ;
( W is sequentially_compact iff T is compact ) by A1, Th16;
hence ( S is compact iff T is compact ) by Th19; :: thesis: verum