let X be TopSpace; :: thesis: for A2, A1, B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 & A1,A2 are_weakly_separated holds
A1 \/ B1,A2 \/ B2 are_weakly_separated
let A2, A1 be Subset of X; :: thesis: for B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 & A1,A2 are_weakly_separated holds
A1 \/ B1,A2 \/ B2 are_weakly_separated
let B1, B2 be Subset of X; :: thesis: ( B1 c= A2 & B2 c= A1 & A1,A2 are_weakly_separated implies A1 \/ B1,A2 \/ B2 are_weakly_separated )
assume A1: ( B1 c= A2 & B2 c= A1 ) ; :: thesis: ( not A1,A2 are_weakly_separated or A1 \/ B1,A2 \/ B2 are_weakly_separated )
assume A1,A2 are_weakly_separated ; :: thesis: A1 \/ B1,A2 \/ B2 are_weakly_separated
then A2: A1 \ A2,A2 \ A1 are_separated by Def7;
( A2 c= A2 \/ B2 & A1 c= A1 \/ B1 ) by XBOOLE_1:7;
then ( B1 c= A2 \/ B2 & B2 c= A1 \/ B1 ) by A1, XBOOLE_1:1;
then A3: ( B1 \ (A2 \/ B2) = {} & B2 \ (A1 \/ B1) = {} ) by XBOOLE_1:37;
( (A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) & (A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/ B1)) ) by XBOOLE_1:42;
then ( (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 & (A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 ) by A3, XBOOLE_1:7, XBOOLE_1:34;
then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated by A2, CONNSP_1:8;
hence A1 \/ B1,A2 \/ B2 are_weakly_separated by Def7; :: thesis: verum