let T be non empty TopSpace; :: thesis: for X being set holds
( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; :: thesis: ( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )
thus ( X is compact Subset of T implies X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) :: thesis: ( X is compact Subset of TopStruct(# the carrier of T, the topology of T #) implies X is compact Subset of T )

proof

assume A1: X is compact Subset of T ; :: thesis: X is compact Subset of TopStruct(# the carrier of T, the topology of T #)
then reconsider Z = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
Z is compact by Th22, A1, Def4;
hence X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: verum

end;

assume A2: X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: X is compact Subset of T
then reconsider Z = X as Subset of T ;
Z is compact by Th22, A2, Def4;
hence X is compact Subset of T ; :: thesis: verum