for X being TopSpace
for A1, A2 being Subset of X holds
( ( A1 misses A2 & A1,A2 are_weakly_separated ) iff A1,A2 are_separated )