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

proof

let F be Subset-Family of TopStruct(# the carrier of T, the topology of T #); :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st
( G c= F & G is Cover of Z & G is finite ) )
assume that
A2: F is Cover of Z and
A3: F is open ; :: thesis: ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of T ;
FF is open by A3, Th32;
then consider G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) such that
A4: G c= FF and
A5: G is Cover of X and
A6: G is finite by A1, A2, Def7;
take G ; :: thesis: ( G c= F & G is Cover of Z & G is finite )
thus ( G c= F & G is Cover of Z & G is finite ) by A4, A5, A6; :: thesis: verum

end;

hence X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: verum

end;

assume A7: 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

proof

let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of Z & G is finite ) )
assume that
A8: F is Cover of Z and
A9: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
FF is open by A9, Th32;
then consider G being Subset-Family of T such that
A10: G c= FF and
A11: G is Cover of X and
A12: G is finite by A7, A8, Def7;
take G ; :: thesis: ( G c= F & G is Cover of Z & G is finite )
thus ( G c= F & G is Cover of Z & G is finite ) by A10, A11, A12; :: thesis: verum

end;

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