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