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