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 holds
( A1,A2 are_weakly_separated iff 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 implies ( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated ) )
assume ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; :: thesis: ( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )
then A1: ( C1 = A1 ` & A1 = C1 ` & C2 = A2 ` & A2 = C2 ` ) by Th4;
thus ( A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated ) :: thesis: ( C1,C2 are_weakly_separated implies A1,A2 are_weakly_separated )

proof

assume A1 \ A2,A2 \ A1 are_separated ; :: according to TSEP_1:def 7 :: thesis: C1,C2 are_weakly_separated
then C2 \ C1,(C2 ` ) \ (C1 ` ) are_separated by A1, Th1;
then C2 \ C1,C1 \ C2 are_separated by Th1;
hence C1,C2 are_weakly_separated by TSEP_1:def 7; :: thesis: verum

end;

assume C1,C2 are_weakly_separated ; :: thesis: A1,A2 are_weakly_separated
then C1 \ C2,C2 \ C1 are_separated by TSEP_1:def 7;
then (C2 ` ) \ (C1 ` ),C2 \ C1 are_separated by Th1;
then A2 \ A1,A1 \ A2 are_separated by A1, Th1;
hence A1,A2 are_weakly_separated by TSEP_1:def 7; :: thesis: verum