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

P \/ Q is compact

let P, Q be Subset of T; :: thesis: ( P is compact & Q is compact implies P \/ Q is compact )

assume that

A1: P is compact and

A2: Q is compact ; :: thesis: P \/ Q is compact

let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of P \/ Q & F is open implies ex G being Subset-Family of T st

( G c= F & G is Cover of P \/ Q & G is finite ) )

assume that

A3: F is Cover of P \/ Q and

A4: F is open ; :: thesis: ex G being Subset-Family of T st

( G c= F & G is Cover of P \/ Q & G is finite )

A5: P \/ Q c= union F by A3, SETFAM_1:def 11;

Q c= P \/ Q by XBOOLE_1:7;

then Q c= union F by A5;

then F is Cover of Q by SETFAM_1:def 11;

then consider G2 being Subset-Family of T such that

A6: G2 c= F and

A7: G2 is Cover of Q and

A8: G2 is finite by A2, A4;

A9: Q c= union G2 by A7, SETFAM_1:def 11;

P c= P \/ Q by XBOOLE_1:7;

then P c= union F by A5;

then F is Cover of P by SETFAM_1:def 11;

then consider G1 being Subset-Family of T such that

A10: G1 c= F and

A11: G1 is Cover of P and

A12: G1 is finite by A1, A4;

reconsider G = G1 \/ G2 as Subset-Family of T ;

take G ; :: thesis: ( G c= F & G is Cover of P \/ Q & G is finite )

thus G c= F by A10, A6, XBOOLE_1:8; :: thesis: ( G is Cover of P \/ Q & G is finite )

P c= union G1 by A11, SETFAM_1:def 11;

then P \/ Q c= (union G1) \/ (union G2) by A9, XBOOLE_1:13;

then P \/ Q c= union (G1 \/ G2) by ZFMISC_1:78;

hence G is Cover of P \/ Q by SETFAM_1:def 11; :: thesis: G is finite

thus G is finite by A12, A8; :: thesis: verum

P \/ Q is compact

let P, Q be Subset of T; :: thesis: ( P is compact & Q is compact implies P \/ Q is compact )

assume that

A1: P is compact and

A2: Q is compact ; :: thesis: P \/ Q is compact

let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of P \/ Q & F is open implies ex G being Subset-Family of T st

( G c= F & G is Cover of P \/ Q & G is finite ) )

assume that

A3: F is Cover of P \/ Q and

A4: F is open ; :: thesis: ex G being Subset-Family of T st

( G c= F & G is Cover of P \/ Q & G is finite )

A5: P \/ Q c= union F by A3, SETFAM_1:def 11;

Q c= P \/ Q by XBOOLE_1:7;

then Q c= union F by A5;

then F is Cover of Q by SETFAM_1:def 11;

then consider G2 being Subset-Family of T such that

A6: G2 c= F and

A7: G2 is Cover of Q and

A8: G2 is finite by A2, A4;

A9: Q c= union G2 by A7, SETFAM_1:def 11;

P c= P \/ Q by XBOOLE_1:7;

then P c= union F by A5;

then F is Cover of P by SETFAM_1:def 11;

then consider G1 being Subset-Family of T such that

A10: G1 c= F and

A11: G1 is Cover of P and

A12: G1 is finite by A1, A4;

reconsider G = G1 \/ G2 as Subset-Family of T ;

take G ; :: thesis: ( G c= F & G is Cover of P \/ Q & G is finite )

thus G c= F by A10, A6, XBOOLE_1:8; :: thesis: ( G is Cover of P \/ Q & G is finite )

P c= union G1 by A11, SETFAM_1:def 11;

then P \/ Q c= (union G1) \/ (union G2) by A9, XBOOLE_1:13;

then P \/ Q c= union (G1 \/ G2) by ZFMISC_1:78;

hence G is Cover of P \/ Q by SETFAM_1:def 11; :: thesis: G is finite

thus G is finite by A12, A8; :: thesis: verum