let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

let A1, A2 be Subset of X; :: thesis: ( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

A1: ( (A1 \/ A2) \ A1 = A2 \ A1 & (A1 \/ A2) \ A2 = A1 \ A2 ) by XBOOLE_1:40;

thus ( A1,A2 are_weakly_separated implies (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ) by A1; :: thesis: ( (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated implies A1,A2 are_weakly_separated )

assume (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ; :: thesis: A1,A2 are_weakly_separated

hence A1,A2 are_weakly_separated by A1; :: thesis: verum

( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

let A1, A2 be Subset of X; :: thesis: ( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

A1: ( (A1 \/ A2) \ A1 = A2 \ A1 & (A1 \/ A2) \ A2 = A1 \ A2 ) by XBOOLE_1:40;

thus ( A1,A2 are_weakly_separated implies (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ) by A1; :: thesis: ( (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated implies A1,A2 are_weakly_separated )

assume (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated ; :: thesis: A1,A2 are_weakly_separated

hence A1,A2 are_weakly_separated by A1; :: thesis: verum