let X be TopSpace; :: thesis: 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; :: thesis: ( ( 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 ) :: thesis: ( A1,A2 are_separated implies ( A1 misses A2 & A1,A2 are_weakly_separated ) )

proof

assume A1: ( A1 misses A2 & A1,A2 are_weakly_separated ) ; :: thesis: A1,A2 are_separated
then ( A1 \ A2 = A1 & A2 \ A1 = A2 ) by XBOOLE_1:83;
hence A1,A2 are_separated by A1, Def7; :: thesis: verum

end;

assume A2: A1,A2 are_separated ; :: thesis: ( A1 misses A2 & A1,A2 are_weakly_separated )
then A1 misses A2 by CONNSP_1:2;
then ( A1 \ A2 = A1 & A2 \ A1 = A2 ) by XBOOLE_1:83;
hence ( A1 misses A2 & A1,A2 are_weakly_separated ) by A2, Def7, CONNSP_1:2; :: thesis: verum