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 A4, A5, TARSKI:def 1; :: 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 A3, SETFAM_1:def 11;
then P \/ (P `) c= (union F) \/ (P `) by XBOOLE_1:9;
then [#] T c= (union F) \/ (P `) by PRE_TOPC:2;
then [#] T = (union F) \/ (P `)
.= (union F) \/ (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 A8, XBOOLE_1:33;
hence G9 c= F by A7; :: thesis: ( G9 is Cover of P & G9 is finite )
(union G) \ (union M) = ([#] T) \ (union {(P `)}) by A9, SETFAM_1:45
.= (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