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

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

( 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

A8:
A /\ B is a_union_of_components of GX
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;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

proof

reconsider Fc = Fa \/ Fb as Subset-Family of GX ;
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

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

end;A9: for B4 being Subset of GX st B4 in Fd holds

B4 is a_component

proof

A10:
A /\ B c= union Fd
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;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

proof

union Fd c= A /\ B
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;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

proof

then
A /\ B = union Fd
by A10;
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;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

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

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