let X be non empty TopSpace; :: thesis: for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds
C1,C2 are_weakly_separated
let A1, A2, C1, C2 be Subset of X; :: thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated implies C1,C2 are_weakly_separated )
assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; :: thesis: ( not A1,A2 are_separated or C1,C2 are_weakly_separated )
assume A1,A2 are_separated ; :: thesis: C1,C2 are_weakly_separated
then A1,A2 are_weakly_separated by TSEP_1:46;
hence C1,C2 are_weakly_separated by A1, Th15; :: thesis: verum