let T be TopStruct ; :: thesis: for P being Subset of T st T is compact & P is closed holds
P is compact

let P be Subset of T; :: thesis: ( T is compact & P is closed implies P is compact )
assume that
A1: T is compact and
A2: P is closed ; :: thesis: P is compact
reconsider pp = {(P `)} as Subset-Family of T ;
let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of P & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite ) )

assume that
A3: F is Cover of P and
A4: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite )

set FP = F \/ pp;
A5: P ` is open by A2;
A6: F \/ pp is open
proof
let H be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not H in F \/ pp or H is open )
assume H in F \/ pp ; :: thesis: H is open
then ( H in F or H in {(P `)} ) by XBOOLE_0:def 3;
hence H is open by ; :: thesis: verum
end;
reconsider M = {(P `)} as Subset-Family of T ;
(F \/ {(P `)}) \ {(P `)} = F \ {(P `)} by XBOOLE_1:40;
then A7: (F \/ {(P `)}) \ {(P `)} c= F by XBOOLE_1:36;
P c= union F by ;
then P \/ (P `) c= () \/ (P `) by XBOOLE_1:9;
then [#] T c= () \/ (P `) by PRE_TOPC:2;
then [#] T = () \/ (P `)
.= () \/ (union {(P `)}) by ZFMISC_1:25
.= union (F \/ {(P `)}) by ZFMISC_1:78 ;
then F \/ pp is Cover of T by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A8: G c= F \/ pp and
A9: G is Cover of T and
A10: G is finite by A1, A6;
reconsider G9 = G \ pp as Subset-Family of T ;
take G9 ; :: thesis: ( G9 c= F & G9 is Cover of P & G9 is finite )
G9 c= (F \/ {(P `)}) \ {(P `)} by ;
hence G9 c= F by A7; :: thesis: ( G9 is Cover of P & G9 is finite )
() \ () = ([#] T) \ (union {(P `)}) by
.= (P `) ` by ZFMISC_1:25
.= P ;
then P c= union G9 by TOPS_2:4;
hence G9 is Cover of P by SETFAM_1:def 11; :: thesis: G9 is finite
thus G9 is finite by A10; :: thesis: verum