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 & C1 \/ C2 = the carrier of X & 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 & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated implies A1,A2 are_separated )

assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; :: thesis: ( not C1 \/ C2 = the carrier of X or not C1,C2 are_weakly_separated or A1,A2 are_separated )

assume C1 \/ C2 = the carrier of X ; :: thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_separated )

then A2: (C1 \/ C2) ` = {} X by XBOOLE_1:37;

( A1 = C1 ` & A2 = C2 ` ) by A1, Th3;

then A1 /\ A2 = {} by A2, XBOOLE_1:53;

then A3: A1 misses A2 ;

assume C1,C2 are_weakly_separated ; :: thesis: A1,A2 are_separated

hence A1,A2 are_separated by A1, A3, Th18; :: thesis: verum

A1,A2 are_separated

let A1, A2, C1, C2 be Subset of X; :: thesis: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated implies A1,A2 are_separated )

assume A1: ( A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition ) ; :: thesis: ( not C1 \/ C2 = the carrier of X or not C1,C2 are_weakly_separated or A1,A2 are_separated )

assume C1 \/ C2 = the carrier of X ; :: thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_separated )

then A2: (C1 \/ C2) ` = {} X by XBOOLE_1:37;

( A1 = C1 ` & A2 = C2 ` ) by A1, Th3;

then A1 /\ A2 = {} by A2, XBOOLE_1:53;

then A3: A1 misses A2 ;

assume C1,C2 are_weakly_separated ; :: thesis: A1,A2 are_separated

hence A1,A2 are_separated by A1, A3, Th18; :: thesis: verum