let GX be TopSpace; for A, B, C being Subset of GX st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
let A, B, C be Subset of GX; ( A,B are_separated & A,C are_separated implies A,B \/ C are_separated )
assume that
A1:
Cl A misses B
and
A2:
A misses Cl B
and
A3:
Cl A misses C
and
A4:
A misses Cl C
; CONNSP_1:def 1 A,B \/ C are_separated
A5:
A /\ (Cl B) = {}
by A2;
A /\ (Cl (B \/ C)) =
A /\ ((Cl B) \/ (Cl C))
by PRE_TOPC:20
.=
(A /\ (Cl B)) \/ (A /\ (Cl C))
by XBOOLE_1:23
.=
{} GX
by A4, A5
;
then A6:
A misses Cl (B \/ C)
;
A7:
(Cl A) /\ B = {}
by A1;
(Cl A) /\ (B \/ C) =
((Cl A) /\ B) \/ ((Cl A) /\ C)
by XBOOLE_1:23
.=
{} GX
by A3, A7
;
then
Cl A misses B \/ C
;
hence
A,B \/ C are_separated
by A6; verum