I define in my draft article Cauchy filters $\mathcal{X}$ on a uniform space $\nu$ by the formula:
$$\mathcal{X}\ne\bot \wedge \mathcal{X}\times^{\mathsf{RLD}}\mathcal{X}\sqsubseteq\nu.$$
$\mathcal{X}\times^{\mathsf{RLD}}\mathcal{X}\sqsubseteq\nu$ can be defined in elementary terms by the formula $$\mathcal{X}\times^{\mathsf{RLD}}\mathcal{X}\sqsubseteq\nu \Leftrightarrow \forall U \in \operatorname{GR}\nu \exists A \in \mathcal{X} : A \times A \subseteq U$$ (here $\operatorname{GR}\nu$ is the set of entourages of the space $\nu$).
But there can be defined a similar formula for funcoids (a generalization of proximity spaces). A filter $\mathcal{X}$ is Cauchy regarding a funcoid $\nu$ iff
$$\mathcal{X}\ne\bot \wedge \mathcal{X}\times^{\mathsf{FCD}}\mathcal{X}\sqsubseteq\nu.$$
This formula can be rewritten in elementary terms for a proximity space $\nu=(U;\delta)$:
$$\mathcal{X}\times^{\mathsf{FCD}}\mathcal{X}\sqsubseteq\nu \Leftrightarrow \forall P, Q \in U : \left( \forall E \in \mathcal{X} : ( E \cap P \neq \emptyset \wedge E \cap Q \neq \emptyset) \Rightarrow P \mathrel{\delta} Q \right).$$
So, I have defined Cauchy filters for proximity spaces.
My question: Am I the first person who has defined Cauchy filters for proximity spaces? If not, please give me references to definition of Cauchy filters on proximity spaces.