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 that
A1: A is a_union_of_components of GX and
A2: 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 )
consider Fa being Subset-Family of GX such that
A3: for Ba being Subset of GX st Ba in Fa holds
Ba is a_component and
A4: A = union Fa by A1, Def2;
consider Fb being Subset-Family of GX such that
A5: for Bb being Subset of GX st Bb in Fb holds
Bb is a_component and
A6: B = union Fb by A2, Def2;
A7: for B2 being Subset of GX st B2 in Fa \/ Fb holds
B2 is a_component

proof

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

end;

A8: A /\ B is a_union_of_components of GX

proof

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

proof

let B4 be Subset of GX; :: thesis: ( B4 in Fd implies B4 is a_component )
assume B4 in Fd ; :: thesis: B4 is a_component
then B4 in Fa by XBOOLE_0:def 4;
hence B4 is a_component by A3; :: thesis: verum

end;

A10: A /\ B c= union Fd

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ B or x in union Fd )
assume A11: x in A /\ B ; :: thesis: x in union Fd
then x in A by XBOOLE_0:def 4;
then consider F1 being set such that
A12: x in F1 and
A13: F1 in Fa by A4, TARSKI:def 4;
reconsider C1 = F1 as Subset of GX by A13;
x in B by A11, XBOOLE_0:def 4;
then consider F2 being set such that
A14: x in F2 and
A15: F2 in Fb by A6, TARSKI:def 4;
reconsider C2 = F2 as Subset of GX by A15;
A16: C2 is a_component by A5, A15;
C1 is a_component by A3, A13;
then A17: ( C1 = C2 or C1 misses C2 ) by A16, CONNSP_1:35;
F1 /\ F2 <> {} by A12, A14, XBOOLE_0:def 4;
then C1 in Fa /\ Fb by A13, A15, A17, XBOOLE_0:def 4;
hence x in union Fd by A12, TARSKI:def 4; :: thesis: verum

end;

union Fd c= A /\ B

proof

let x be object ; :: 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
A18: x in X4 and
A19: X4 in Fd by TARSKI:def 4;
X4 in Fb by A19, XBOOLE_0:def 4;
then A20: x in union Fb by A18, TARSKI:def 4;
X4 in Fa by A19, XBOOLE_0:def 4;
then x in union Fa by A18, TARSKI:def 4;
hence x in A /\ B by A4, A6, A20, XBOOLE_0:def 4; :: thesis: verum

end;

then A /\ B = union Fd by A10;
hence A /\ B is a_union_of_components of GX by A9, Def2; :: thesis: verum

end;

reconsider Fc = Fa \/ Fb as Subset-Family of GX ;
A \/ B = union Fc by A4, A6, ZFMISC_1:78;
hence ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) by A7, A8, Def2; :: thesis: verum