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 )

then reconsider Z = X as Subset of T ;

Z is compact by Th22, A2, Def4;

hence X is compact Subset of T ; :: thesis: verum

( 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 A2:
X is compact Subset of TopStruct(# the carrier of T, the topology of T #)
; :: thesis: X is compact Subset of T
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;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

then reconsider Z = X as Subset of T ;

Z is compact by Th22, A2, Def4;

hence X is compact Subset of T ; :: thesis: verum