let X be TopSpace; :: thesis: for A1, A2, B being Subset of st ( A1,B are_separated or A2,B are_separated ) holds
A1 /\ A2,B are_separated
let A1, A2, B be Subset of ; :: thesis: ( ( 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 ) :: thesis: verum
proof
A1: now
A2: A1 /\ A2 c= A2 by XBOOLE_1:17;
assume A2,B are_separated ; :: thesis: ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated )
hence ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated ) by A2, CONNSP_1:8; :: thesis: verum
end;
A3: now
A4: A1 /\ A2 c= A1 by XBOOLE_1:17;
assume A1,B are_separated ; :: thesis: ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated )
hence ( ( A1,B are_separated or A2,B are_separated ) implies A1 /\ A2,B are_separated ) by A4, CONNSP_1:8; :: thesis: verum
end;
assume ( A1,B are_separated or A2,B are_separated ) ; :: thesis: A1 /\ A2,B are_separated
hence A1 /\ A2,B are_separated by A3, A1; :: thesis: verum
end;