let X be TopSpace; :: thesis:
let A1, A2, B be Subset of X; :: thesis:
thus ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated ) :: thesis:

A1: now :: thesis:

A2: A1 /\ A2 c= A2 by XBOOLE_1:17;
assume A2,B are_separated ; :: thesis:
hence ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated ) by A2, CONNSP_1:7; :: thesis:

end;

A3: now :: thesis:

A4: A1 /\ A2 c= A1 by XBOOLE_1:17;
assume A1,B are_separated ; :: thesis:
hence ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated ) by A4, CONNSP_1:7; :: thesis:

end;

assume ( A1,B are_separated or A2,B are_separated ) ; :: thesis:
hence A1 /\ A2,B are_separated by A3, A1; :: thesis:

end;