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 7 :: 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, TOPS_1:29;
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, TOPS_2: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 12;
then P \/ (P ` ) c= (union F) \/ (P ` ) by XBOOLE_1:9;
then [#] T c= (union F) \/ (P ` ) by PRE_TOPC:18;
then [#] T = (union F) \/ (P ` ) by XBOOLE_0:def 10
.= (union F) \/ (union {(P ` )}) by ZFMISC_1:31
.= union (F \/ {(P ` )}) by ZFMISC_1:96 ;
then F \/ pp is Cover of T by SETFAM_1:def 12;
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, Def3;
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, XBOOLE_1:1; :: thesis: ( G9 is Cover of P & G9 is finite )
(union G) \ (union M) = ([#] T) \ (union {(P ` )}) by A9, SETFAM_1:60
.= (P ` ) ` by ZFMISC_1:31
.= P ;
then P c= union G9 by TOPS_2:6;
hence G9 is Cover of P by SETFAM_1:def 12; :: thesis: G9 is finite
thus G9 is finite by A10; :: thesis: verum