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

(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

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

reconsider M = {(P `)} as Subset-Family of T ;
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;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

(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