let X be TopSpace; :: thesis: for A1, A2, C being Subset of X st A1,A2 are_weakly_separated holds
A1 \/ C,A2 \/ C are_weakly_separated
let A1, A2, C be Subset of X; :: thesis: ( A1,A2 are_weakly_separated implies A1 \/ C,A2 \/ C are_weakly_separated )
assume A1,A2 are_weakly_separated ; :: thesis: A1 \/ C,A2 \/ C are_weakly_separated
then A1: A1 \ A2,A2 \ A1 are_separated by Def7;
A2: (A1 \/ C) \ (A2 \/ C) = (A1 \ (A2 \/ C)) \/ (C \ (A2 \/ C)) by XBOOLE_1:42
.= (A1 \ (A2 \/ C)) \/ {} by XBOOLE_1:46
.= (A1 \ A2) /\ (A1 \ C) by XBOOLE_1:53 ;
(A2 \/ C) \ (A1 \/ C) = (A2 \ (A1 \/ C)) \/ (C \ (A1 \/ C)) by XBOOLE_1:42
.= (A2 \ (A1 \/ C)) \/ {} by XBOOLE_1:46
.= (A2 \ A1) /\ (A2 \ C) by XBOOLE_1:53 ;
then ( (A1 \/ C) \ (A2 \/ C) c= A1 \ A2 & (A2 \/ C) \ (A1 \/ C) c= A2 \ A1 ) by A2, XBOOLE_1:17;
then (A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated by A1, CONNSP_1:8;
hence A1 \/ C,A2 \/ C are_weakly_separated by Def7; :: thesis: verum