let X be non empty TopSpace; :: thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; :: thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_separated )
assume A1: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition ) ; :: thesis: ( not X1 misses X2 or not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume A2: X1 misses X2 ; :: thesis: ( not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume Y1,Y2 are_weakly_separated ; :: thesis: X1,X2 are_separated
then X1,X2 are_weakly_separated by A1, Th39;
hence X1,X2 are_separated by A2, TSEP_1:78; :: thesis: verum