let X be non empty TopSpace; :: thesis: for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds
A1,A2 are_weakly_separated
let A1, A2, C1, C2 be Subset of X; :: thesis: ( C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated implies A1,A2 are_weakly_separated )
assume A1: ( C1 c= A1 & C2 c= A2 ) ; :: thesis: ( not C1 \/ C2 = A1 \/ A2 or not C1,C2 are_weakly_separated or A1,A2 are_weakly_separated )
assume A2: C1 \/ C2 = A1 \/ A2 ; :: thesis: ( not C1,C2 are_weakly_separated or A1,A2 are_weakly_separated )
assume C1,C2 are_weakly_separated ; :: thesis: A1,A2 are_weakly_separated
then A3: (A1 \/ A2) \ C1,(A1 \/ A2) \ C2 are_separated by A2, Th22;
( (A1 \/ A2) \ A1 c= (A1 \/ A2) \ C1 & (A1 \/ A2) \ A2 c= (A1 \/ A2) \ C2 ) by A1, XBOOLE_1:34;
then (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A3, CONNSP_1:8;
hence A1,A2 are_weakly_separated by Th22; :: thesis: verum