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 ;
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 ;
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 ;
reconsider C1 = F1 as Subset of GX by A13;
x in B by ;
then consider F2 being set such that
A14: x in F2 and
A15: F2 in Fb by ;
reconsider C2 = F2 as Subset of GX by A15;
A16: C2 is a_component by ;
C1 is a_component by ;
then A17: ( C1 = C2 or C1 misses C2 ) by ;
F1 /\ F2 <> {} by ;
then C1 in Fa /\ Fb by ;
hence x in union Fd by ; :: 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 ;
then A20: x in union Fb by ;
X4 in Fa by ;
then x in union Fa by ;
hence x in A /\ B by ; :: thesis: verum
end;
then A /\ B = union Fd by A10;
hence A /\ B is a_union_of_components of GX by ; :: thesis: verum
end;
reconsider Fc = Fa \/ Fb as Subset-Family of GX ;
A \/ B = union Fc by ;
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