Cauchy filters defined for proximity spaces?

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.

• Hm... maybe all proximity spaces are totally bounded? We need examples or counter-examples – porton Feb 28 '14 at 19:55