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 7 :: 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 12;
P c= P \/ Q by XBOOLE_1:7;
then P c= union F by A5, XBOOLE_1:1;
then F is Cover of P by SETFAM_1:def 12;
then consider G1 being Subset-Family of T such that
A6: G1 c= F and
A7: G1 is Cover of P and
A8: G1 is finite by A1, A4, Def7;
Q c= P \/ Q by XBOOLE_1:7;
then Q c= union F by A5, XBOOLE_1:1;
then F is Cover of Q by SETFAM_1:def 12;
then consider G2 being Subset-Family of T such that
A9: G2 c= F and
A10: G2 is Cover of Q and
A11: G2 is finite by A2, A4, Def7;
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 A6, A9, XBOOLE_1:8; :: thesis: ( G is Cover of P \/ Q & G is finite )
( P c= union G1 & Q c= union G2 ) by A7, A10, SETFAM_1:def 12;
then P \/ Q c= (union G1) \/ (union G2) by XBOOLE_1:13;
then P \/ Q c= union (G1 \/ G2) by ZFMISC_1:96;
hence G is Cover of P \/ Q by SETFAM_1:def 12; :: thesis: G is finite
thus G is finite by A8, A11; :: thesis: verum