let X be TopSpace; :: thesis: for A1, A2, 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 A1, A2 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 that
A1: B1 c= A2 and
A2: B2 c= A1 ; :: thesis: ( not A1,A2 are_weakly_separated or A1 \/ B1,A2 \/ B2 are_weakly_separated )
A2 c= A2 \/ B2 by XBOOLE_1:7;
then B1 c= A2 \/ B2 by A1, XBOOLE_1:1;
then A3: B1 \ (A2 \/ B2) = {} by XBOOLE_1:37;
A1 c= A1 \/ B1 by XBOOLE_1:7;
then B2 c= A1 \/ B1 by A2, XBOOLE_1:1;
then A4: B2 \ (A1 \/ B1) = {} by XBOOLE_1:37;
(A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/ B1)) by XBOOLE_1:42;
then A5: (A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 by A4, XBOOLE_1:7, XBOOLE_1:34;
(A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) by XBOOLE_1:42;
then A6: (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 by A3, XBOOLE_1:7, XBOOLE_1:34;
assume A1,A2 are_weakly_separated ; :: thesis: A1 \/ B1,A2 \/ B2 are_weakly_separated
then A1 \ A2,A2 \ A1 are_separated ;
then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated by A6, A5, CONNSP_1:7;
hence A1 \/ B1,A2 \/ B2 are_weakly_separated ; :: thesis: verum