Closed-neighborhood shrinking in a normal space (source code)

= Closed-neighborhood shrinking in a normal space
{title2=$F\subset W\subset\overline W\subset U$}

If $F$ is closed, $U$ is open, and $F\subset U$ in a <normal topological space>, separate $F$ from the closed complement $X\setminus U$ by disjoint open sets $W,V$. Then $\overline W\subset X\setminus V\subset U$. In particular, first separate two disjoint closed sets by disjoint open sets and then shrink each neighborhood this way: their closures are disjoint. No additional metric or compactness assumption is needed.