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;

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; :: thesis: verum

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;

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; :: thesis: verum