let X be TopSpace; :: thesis: for A1, A2, B being Subset of X st A1,B are_weakly_separated & A2,B are_weakly_separated holds
A1 \/ A2,B are_weakly_separated
let A1, A2, B be Subset of X; :: thesis: ( A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 \/ A2,B are_weakly_separated )
thus
( A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 \/ A2,B are_weakly_separated )
:: thesis: verumproof
assume
(
A1,
B are_weakly_separated &
A2,
B are_weakly_separated )
;
:: thesis: A1 \/ A2,B are_weakly_separated
then
(
A1 \ B,
B \ A1 are_separated &
A2 \ B,
B \ A2 are_separated )
by Def7;
then
(
A1 \ B,
(B \ A1) /\ (B \ A2) are_separated &
A2 \ B,
(B \ A1) /\ (B \ A2) are_separated )
by Th44;
then
(A1 \ B) \/ (A2 \ B),
(B \ A1) /\ (B \ A2) are_separated
by Th45;
then
(A1 \/ A2) \ B,
(B \ A1) /\ (B \ A2) are_separated
by XBOOLE_1:42;
then
(A1 \/ A2) \ B,
B \ (A1 \/ A2) are_separated
by XBOOLE_1:53;
hence
A1 \/ A2,
B are_weakly_separated
by Def7;
:: thesis: verum
end;