let X be TopSpace; for A1, A2, B being Subset of X st ( A1,B are_separated or A2,B are_separated ) holds
A1 /\ A2,B are_separated
let A1, A2, B be Subset of X; ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated )
thus
( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated )
verum