let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )
let A, B be Subset of GX; :: thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) )
assume A1: ( A is a_union_of_components of GX & B is a_union_of_components of GX ) ; :: thesis: ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )
then consider Fa being Subset-Family of GX such that
A2: ( ( for Ba being Subset of GX st Ba in Fa holds
Ba is_a_component_of GX ) & A = union Fa ) by Def2;
consider Fb being Subset-Family of GX such that
A3: ( ( for Bb being Subset of GX st Bb in Fb holds
Bb is_a_component_of GX ) & B = union Fb ) by A1, Def2;
reconsider Fc = Fa \/ Fb as Subset-Family of GX ;
A4: A \/ B = union Fc by A2, A3, ZFMISC_1:96;
A5: for B2 being Subset of GX st B2 in Fa \/ Fb holds
B2 is_a_component_of GX

proof

let B2 be Subset of GX; :: thesis: ( B2 in Fa \/ Fb implies B2 is_a_component_of GX )
assume B2 in Fa \/ Fb ; :: thesis: B2 is_a_component_of GX
then ( B2 in Fa or B2 in Fb ) by XBOOLE_0:def 3;
hence B2 is_a_component_of GX by A2, A3; :: thesis: verum

end;

A /\ B is a_union_of_components of GX

proof

reconsider Fd = Fa /\ Fb as Subset-Family of GX ;
A6: for B4 being Subset of GX st B4 in Fd holds
B4 is_a_component_of GX

proof

let B4 be Subset of GX; :: thesis: ( B4 in Fd implies B4 is_a_component_of GX )
assume B4 in Fd ; :: thesis: B4 is_a_component_of GX
then ( B4 in Fa & B4 in Fb ) by XBOOLE_0:def 4;
hence B4 is_a_component_of GX by A2; :: thesis: verum

end;

A /\ B = union Fd

proof

A7: A /\ B c= union Fd

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ B or x in union Fd )
assume x in A /\ B ; :: thesis: x in union Fd
then A8: ( x in A & x in B ) by XBOOLE_0:def 4;
then consider F1 being set such that
A9: ( x in F1 & F1 in Fa ) by A2, TARSKI:def 4;
consider F2 being set such that
A10: ( x in F2 & F2 in Fb ) by A3, A8, TARSKI:def 4;
A11: F1 /\ F2 <> {} by A9, A10, XBOOLE_0:def 4;
reconsider C1 = F1 as Subset of GX by A9;
reconsider C2 = F2 as Subset of GX by A10;
A12: C1 is_a_component_of GX by A2, A9;
C2 is_a_component_of GX by A3, A10;
then ( C1 = C2 or C1 misses C2 ) by A12, CONNSP_1:37;
then C1 in Fa /\ Fb by A9, A10, A11, XBOOLE_0:def 4, XBOOLE_0:def 7;
hence x in union Fd by A9, TARSKI:def 4; :: thesis: verum

end;

union Fd c= A /\ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union Fd or x in A /\ B )
assume x in union Fd ; :: thesis: x in A /\ B
then consider X4 being set such that
A13: ( x in X4 & X4 in Fd ) by TARSKI:def 4;
A14: ( X4 in Fa & X4 in Fb ) by A13, XBOOLE_0:def 4;
then A15: x in union Fa by A13, TARSKI:def 4;
x in union Fb by A13, A14, TARSKI:def 4;
hence x in A /\ B by A2, A3, A15, XBOOLE_0:def 4; :: thesis: verum

end;

hence A /\ B = union Fd by A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence A /\ B is a_union_of_components of GX by A6, Def2; :: thesis: verum

end;

hence ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) by A4, A5, Def2; :: thesis: verum