let X be TopSpace; :: thesis: for A1, A2, C being Subset of X st A1,A2 are_separated holds
A1 /\ C,A2 /\ C are_separated
let A1, A2, C be Subset of X; :: thesis: ( A1,A2 are_separated implies A1 /\ C,A2 /\ C are_separated )
A1: ( A1 /\ C c= A1 & A2 /\ C c= A2 ) by XBOOLE_1:17;
assume A1,A2 are_separated ; :: thesis: A1 /\ C,A2 /\ C are_separated
hence A1 /\ C,A2 /\ C are_separated by A1, CONNSP_1:7; :: thesis: verum