let X be TopSpace; for A1, A2 being Subset of X holds
( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )
let A1, A2 be Subset of X; ( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )
thus
( A1 misses A2 & A1,A2 are_weakly_separated implies A1,A2 are_separated )
( A1,A2 are_separated implies ( A1 misses A2 & A1,A2 are_weakly_separated ) )
assume A3:
A1,A2 are_separated
; ( A1 misses A2 & A1,A2 are_weakly_separated )
then
A1 misses A2
by CONNSP_1:1;
then
( A1 \ A2 = A1 & A2 \ A1 = A2 )
by XBOOLE_1:83;
hence
( A1 misses A2 & A1,A2 are_weakly_separated )
by A3, CONNSP_1:1; verum