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

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

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

A1: A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47;

A2: A1 \ (A1 /\ A2) = A1 \ A2 by XBOOLE_1:47;

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

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

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

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

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

A1: A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47;

A2: A1 \ (A1 /\ A2) = A1 \ A2 by XBOOLE_1:47;

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

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

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