let GX be TopSpace; :: thesis: 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; :: thesis: ( 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 ; :: according to CONNSP_1:def 1 :: thesis: A,B \/ C are_separated
A5: A /\ (Cl B) = {} by A2, XBOOLE_0:def 7;
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, XBOOLE_0:def 7 ;
then A6: A misses Cl (B \/ C) by XBOOLE_0:def 7;
A7: (Cl A) /\ B = {} by A1, XBOOLE_0:def 7;
(Cl A) /\ (B \/ C) = ((Cl A) /\ B) \/ ((Cl A) /\ C) by XBOOLE_1:23
.= {} GX by A3, A7, XBOOLE_0:def 7 ;
then Cl A misses B \/ C by XBOOLE_0:def 7;
hence A,B \/ C are_separated by A6, Def1; :: thesis: verum