let X be non empty TopSpace; 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; ( 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 )
; ( 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
; ( 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
; A1,A2 are_separated
hence
A1,A2 are_separated
by A1, A3, Th18; verum