let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1,X2 are_weakly_separated iff X1,X2 are_separated )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 constitute_a_decomposition implies ( X1,X2 are_weakly_separated iff X1,X2 are_separated ) )
assume X1,X2 constitute_a_decomposition ; :: thesis: ( X1,X2 are_weakly_separated iff X1,X2 are_separated )
then X1 misses X2 by Th30;
hence ( X1,X2 are_weakly_separated iff X1,X2 are_separated ) by TSEP_1:85; :: thesis: verum