[proofplan] We prove each direction separately. For the forward direction, we use the [Neighbourhood Characterisation of Closure](/theorems/1005) to build a net indexed by the neighbourhood system of $x$, directed by reverse inclusion. For the converse, we show that any open set containing $x$ must eventually contain the net, forcing it to meet $A$. [/proofplan] [step:Construct a net from the neighbourhood system of $x$ when $x \in \overline{A}$] Assume $x \in \overline{A}$. Define the index set $D := \{U \in \tau : x \in U\}$, the collection of all open neighbourhoods of $x$. We direct $D$ by reverse inclusion: $U \preceq V$ if and only if $V \subset U$. This is a directed set: for any $U_1, U_2 \in D$, the intersection $U_1 \cap U_2$ belongs to $D$ (since $\tau$ is closed under finite intersections and $x \in U_1 \cap U_2$) and satisfies $U_1 \preceq U_1 \cap U_2$ and $U_2 \preceq U_1 \cap U_2$. By the [Neighbourhood Characterisation of Closure](/theorems/1005), every $U \in D$ satisfies $U \cap A \neq \varnothing$. For each $U \in D$, choose a point $s_U \in U \cap A$ (invoking the Axiom of Choice on the family $\{U \cap A\}_{U \in D}$). This defines a net \begin{align*} s: D &\to A \\ U &\mapsto s_U. \end{align*} We verify that $s_U \to x$. Let $V \in \tau$ with $x \in V$. Then $V \in D$, and for every $U \in D$ with $V \preceq U$ (i.e., $U \subset V$), we have $s_U \in U \cap A \subset U \subset V$. Thus $s_U \in V$ for all $U \succeq V$, confirming $s_U \to x$ in $(X, \tau)$. [guided] Assume $x \in \overline{A}$. We need to produce a net in $A$ converging to $x$. The natural index set is the system of open neighbourhoods of $x$, since the closure condition guarantees each neighbourhood meets $A$. Define $D := \{U \in \tau : x \in U\}$. We equip $D$ with the partial order $U \preceq V$ if and only if $V \subset U$ (reverse inclusion). Why reverse inclusion? Because we want smaller neighbourhoods to come "later" in the directed set, so that convergence forces the net values to eventually lie in any prescribed neighbourhood of $x$. We verify that $(D, \preceq)$ is a directed set. The key axiom to check is that every pair has an upper bound: given $U_1, U_2 \in D$, their intersection $U_1 \cap U_2$ is open (since $\tau$ is closed under finite intersections), contains $x$ (since $x \in U_1$ and $x \in U_2$), and satisfies $U_1 \cap U_2 \subset U_1$ and $U_1 \cap U_2 \subset U_2$. Therefore $U_1 \preceq U_1 \cap U_2$ and $U_2 \preceq U_1 \cap U_2$, so $U_1 \cap U_2$ is a common upper bound. By the [Neighbourhood Characterisation of Closure](/theorems/1005), since $x \in \overline{A}$, every open set $U$ containing $x$ satisfies $U \cap A \neq \varnothing$. Using the Axiom of Choice on the non-empty family $\{U \cap A : U \in D\}$, we select for each $U \in D$ an element $s_U \in U \cap A$. This defines a net $s: D \to A$, $U \mapsto s_U$. To verify convergence $s_U \to x$: let $V$ be any open set containing $x$. Then $V \in D$. For any $U \succeq V$ in the directed set (meaning $U \subset V$), we have $s_U \in U \cap A \subset U \subset V$. So $s_U \in V$ for all $U \succeq V$, which is precisely the definition of $s_U \to x$. [/guided] [/step] [step:Show that a convergent net in $A$ forces the limit into $\overline{A}$] Conversely, suppose $(s_\alpha)_{\alpha \in D}$ is a net in $A$ with $s_\alpha \to x$. Let $U \in \tau$ with $x \in U$. By the definition of net convergence, there exists $\alpha_0 \in D$ such that $s_\alpha \in U$ for all $\alpha \succeq \alpha_0$. In particular, $s_{\alpha_0} \in U$. Since $s_{\alpha_0} \in A$, we obtain $s_{\alpha_0} \in U \cap A$, so $U \cap A \neq \varnothing$. Since $U$ was an arbitrary open neighbourhood of $x$, the [Neighbourhood Characterisation of Closure](/theorems/1005) gives $x \in \overline{A}$. [guided] Conversely, suppose a net $(s_\alpha)_{\alpha \in D}$ in $A$ converges to $x$. We must show $x \in \overline{A}$. By the [Neighbourhood Characterisation of Closure](/theorems/1005), it suffices to show that every open neighbourhood of $x$ meets $A$. Let $U \in \tau$ with $x \in U$. Since $s_\alpha \to x$, there exists $\alpha_0 \in D$ such that $s_\alpha \in U$ for all $\alpha \succeq \alpha_0$. In particular, $s_{\alpha_0} \in U$. But every term of the net lies in $A$ by assumption, so $s_{\alpha_0} \in U \cap A$. This shows $U \cap A \neq \varnothing$. Since $U$ was arbitrary, the neighbourhood characterisation gives $x \in \overline{A}$. Note that this direction does not require the Axiom of Choice — the net is given to us, and we simply read off its properties. [/guided] [/step]