let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff A1,A2 are_separated )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 constitute_a_decomposition implies ( A1,A2 are_weakly_separated iff A1,A2 are_separated ) )
assume A1,A2 constitute_a_decomposition ; :: thesis: ( A1,A2 are_weakly_separated iff A1,A2 are_separated )
then A1 misses A2 by Def1;
hence ( A1,A2 are_weakly_separated iff A1,A2 are_separated ) by TSEP_1:46; :: thesis: verum