let GX be non empty TopSpace; 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; ( 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
; ( 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
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
A10:
A /\ B c= union Fd
proof
let x be
object ;
TARSKI:def 3 ( not x in A /\ B or x in union Fd )
assume A11:
x in A /\ B
;
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;
verum
end;
union Fd c= A /\ B
then
A /\ B = union Fd
by A10;
hence
A /\ B is
a_union_of_components of
GX
by A9, Def2;
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; verum