let X be TopSpace; 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; ( A1,A2 are_weakly_separated implies A1 \/ C,A2 \/ C are_weakly_separated )
(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
;
then A1:
(A1 \/ C) \ (A2 \/ C) c= A1 \ A2
by XBOOLE_1:17;
(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 A2:
(A2 \/ C) \ (A1 \/ C) c= A2 \ A1
by XBOOLE_1:17;
assume
A1,A2 are_weakly_separated
; A1 \/ C,A2 \/ C are_weakly_separated
then
A1 \ A2,A2 \ A1 are_separated
;
then
(A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated
by A1, A2, CONNSP_1:7;
hence
A1 \/ C,A2 \/ C are_weakly_separated
; verum