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

proof

assume that
A1: A1,B are_weakly_separated and
A2: A2,B are_weakly_separated ; :: thesis: A1 /\ A2,B are_weakly_separated
A2 \ B,B \ A2 are_separated by A2;
then A3: (A1 \ B) /\ (A2 \ B),B \ A2 are_separated by Th40;
A1 \ B,B \ A1 are_separated by A1;
then (A1 \ B) /\ (A2 \ B),B \ A1 are_separated by Th40;
then (A1 \ B) /\ (A2 \ B),(B \ A1) \/ (B \ A2) are_separated by A3, Th41;
then (A1 /\ A2) \ B,(B \ A1) \/ (B \ A2) are_separated by Lm2;
then (A1 /\ A2) \ B,B \ (A1 /\ A2) are_separated by XBOOLE_1:54;
hence A1 /\ A2,B are_weakly_separated ; :: thesis: verum

end;