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 & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & 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 & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated implies X1,X2 are_separated )
assume A1: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition ) ; :: thesis: ( not Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) or not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
assume Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) ; :: thesis: ( not Y1,Y2 are_weakly_separated or X1,X2 are_separated )
then A2: X1 misses X2 by A1, Th32;
assume Y1,Y2 are_weakly_separated ; :: thesis: X1,X2 are_separated
hence X1,X2 are_separated by A1, A2, Th39; :: thesis: verum