A Cauchy net which has a convergent subnet

I think that this question has been asked many times before but I want to know whether my argument is correct.

I want to show that a Cauchy net $\{x_{\lambda}\}$ has a cluster point iff it has subnet which converges to $y$.

Proof. Let $y$ be a cluster point of $\{x_{\lambda}\}$. Define $M := \{(\lambda, U):\lambda \in \Lambda, U \text{ a neighborhood of } y \text{ such that } x_{\lambda} \in U\}$, and order M as follows: $(\lambda_1, U_1) \leq (\lambda_2, U_2)$ if and only if $\lambda_1 \leq \lambda_2$ and $U_2 \subseteq U1$. This is easily verified to be a direction on M. Define $\phi : M \to \Lambda$ by $\phi(\lambda, U) = \lambda$. Then $\phi$ is increasing and cofinal in $\Lambda$. So $\phi$ defines a subnet of $\{x_{\lambda}\}$. Let $U_0$ be any neighborhood of $y$ and find $\lambda_0 \in \Lambda$ such that $x_{\lambda_0} \in U_0$. Then $(\lambda_0, U_0) \in M$, and moreover, $(\lambda, U) \geq (\lambda_0, U_0)$ implies $U \subseteq U_0$, so that $x_{\lambda} \in U \subseteq U_0$. It follows that the subnet defined by $\phi$ converges to $y$.

Suppose $\phi : M \to \Lambda$ defines a subnet of a Cauchy net $\{x_{\lambda}\}$ which converges to $y$. Then for each neighborhood $U$ of $y$, there is some $\alpha_U$ in M such that $\alpha \geq \alpha_U$ implies $x_{\phi(\alpha)} \in U$. Suppose a neighborhood $U$ of $y$ and a point $\lambda_0 \in \Lambda$ are given. Since $\phi(M)$ is cofinal in $\Lambda$, there is some $\alpha_0 \in M$ such that $\phi(\alpha_0) \geq \lambda_0$. But there is also some $\alpha_U \in M$ such that $\alpha \geq \alpha_U$ implies $\phi(\alpha) \in U$. Pick $\alpha^* = \max\{\alpha_0, \alpha_U\}$. Then $\phi(\alpha^*) \geq \lambda$ and $\alpha^* \geq \alpha_U$. So, $x_{\phi(\alpha^*)} \in U$. It follows that $y$ is a cluster point of Cauchy net $\{x_\lambda\}$.