let X be non empty TopSpace; 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; ( 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; ( A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated implies A1,A2 are_weakly_separated )
assume
A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated
; A1,A2 are_weakly_separated
hence
A1,A2 are_weakly_separated
by A2, A1; verum