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 & A1 misses A2 & C1,C2 are_weakly_separated holds
A1,A2 are_separated
let A1, A2, C1, C2 be Subset of X; :: thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated )
assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; :: thesis: ( not A1 misses A2 or not C1,C2 are_weakly_separated or A1,A2 are_separated )
assume A2: A1 /\ A2 = {} ; :: according to XBOOLE_0:def 7 :: thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_separated )
assume C1,C2 are_weakly_separated ; :: thesis: A1,A2 are_separated
then A3: A1,A2 are_weakly_separated by A1, Th15;
A1 misses A2 by A2;
hence A1,A2 are_separated by A3, TSEP_1:46; :: thesis: verum