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 & A1,A2 are_weakly_separated holds

C1,C2 are_weakly_separated

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

assume ( C1 c= A1 & C2 c= A2 ) ; :: thesis: ( not C1 /\ C2 = A1 /\ A2 or not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )

then A1: ( C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2) ) by XBOOLE_1:33;

assume A2: C1 /\ C2 = A1 /\ A2 ; :: thesis: ( not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )

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

then A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2, Th23;

then C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A1, CONNSP_1:7;

hence C1,C2 are_weakly_separated by Th23; :: thesis: verum

C1,C2 are_weakly_separated

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

assume ( C1 c= A1 & C2 c= A2 ) ; :: thesis: ( not C1 /\ C2 = A1 /\ A2 or not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )

then A1: ( C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2) ) by XBOOLE_1:33;

assume A2: C1 /\ C2 = A1 /\ A2 ; :: thesis: ( not A1,A2 are_weakly_separated or C1,C2 are_weakly_separated )

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

then A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2, Th23;

then C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A1, CONNSP_1:7;

hence C1,C2 are_weakly_separated by Th23; :: thesis: verum