let X be TopSpace; :: thesis: for A1, A2, B being Subset of X holds
( ( A1,B are_separated & A2,B are_separated ) iff A1 \/ A2,B are_separated )
let A1, A2, B be Subset of X; :: thesis: ( ( A1,B are_separated & A2,B are_separated ) iff A1 \/ A2,B are_separated )
( A1 \/ A2,B are_separated implies ( A1,B are_separated & A2,B are_separated ) )
proof
A1: ( A1 c= A1 \/ A2 & A2 c= A1 \/ A2 ) by XBOOLE_1:7;
assume A1 \/ A2,B are_separated ; :: thesis: ( A1,B are_separated & A2,B are_separated )
hence ( A1,B are_separated & A2,B are_separated ) by A1, CONNSP_1:7; :: thesis: verum
end;
hence ( ( A1,B are_separated & A2,B are_separated ) iff A1 \/ A2,B are_separated ) by CONNSP_1:8; :: thesis: verum