let T be non empty TopSpace; :: thesis: for X being set holds
( X is compact Subset of iff X is compact Subset of )
let X be set ; :: thesis: ( X is compact Subset of iff X is compact Subset of )
thus ( X is compact Subset of implies X is compact Subset of ) :: thesis: ( X is compact Subset of implies X is compact Subset of )

proof

assume A1: X is compact Subset of ; :: thesis: X is compact Subset of
then reconsider Z = X as Subset of ;
Z is compact

proof

let F be Subset-Family of ; :: according to COMPTS_1:def 7 :: thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of 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 st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of ;
FF is open by A3, Th32;
then consider G being Subset-Family of 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 ; :: thesis: verum

end;

assume A7: X is compact Subset of ; :: thesis: X is compact Subset of
then reconsider Z = X as Subset of ;
Z is compact

proof

let F be Subset-Family of ; :: according to COMPTS_1:def 7 :: thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of 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 st
( G c= F & G is Cover of Z & G is finite )
reconsider FF = F as Subset-Family of ;
FF is open by A9, Th32;
then consider G being Subset-Family of 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 ; :: thesis: verum