A metric on a nonempty set generates an entourage uniformity whose induced topology and uniformly continuous maps are the usual metric notions, and this uniformity is separated

The diagonal lies in every $E_{\epsilon }$, inverses agree with $E_{\epsilon }$ by symmetry, intersections contain $E_{\min (\epsilon ,\delta )}$, and $E_{\epsilon \mathrm{/}2}\circ E_{\epsilon \mathrm{/}2}\subseteq E_{\epsilon }$ by the triangle inequality.

The family $(E_{\epsilon }{)}_{\epsilon >0}$ is nonempty, none of its members is empty because $X\mathrm{\ne }\mathrm{\varnothing }$, and it is downward directed by step 1.1, so [L4] makes its upward closure a filter. The diagonal, inverse, and square-root properties in step 1.1 then make it a uniformity. Its $E_{\epsilon }[x]$ are precisely metric balls, so its induced topology is the metric topology by [L2] and [L5].

The intersection of all $E_{\epsilon }$ is the diagonal, since $d(x,y)>0$ for $x\mathrm{\ne }y$ and $E_{d(x,y)\mathrm{/}2}$ excludes $(x,y)$; hence the uniformity is separated.

The defining entourage implication for $E_{\delta }$ and $E_{\epsilon }$ is exactly the quantified condition of [L3], which proves the final equivalence.