proximity generated by uniformity

Definition. Let $X$ be a uniform space with uniformity $𝒰$. The uniform proximity, or proximity generated by $\mathrm{U}$, is a binary relation $𝛿$ on the subsets of $X$, given by the formula

$$A𝛿B\mathit{\hspace{1em}\hspace{1em}}\iff \mathit{\hspace{1em}\hspace{1em}}\forall U\in 𝒰:U\cap (A\times B)\ne \mathrm{\varnothing }.$$

Correctness of the above proximity is given by the below theorem:

Theorem. Proximity generated by a uniformity is a proximity. In other words, $X$ is a proximity space with proximity $𝛿$.