[proofplan] The forward direction uses the topological definition of continuity (preimages of open sets are open) to show that the image net is eventually in every open neighbourhood of $f(x)$. The converse proceeds by contrapositive: if $f$ is not continuous, there exists an open set $V \subset Y$ whose preimage $f^{-1}(V)$ is not open, and we build a net converging to a point of $f^{-1}(V)$ whose image fails to enter $V$. [/proofplan] [step:Show that continuity forces image nets to converge] Assume $f$ is continuous, and let $(s_\alpha)_{\alpha \in D}$ be a net in $X$ with $s_\alpha \to x$. Let $V \in \tau_Y$ with $f(x) \in V$. Since $f$ is continuous, the preimage $f^{-1}(V)$ is open in $X$ and contains $x$. By convergence of $(s_\alpha)$ to $x$, there exists $\alpha_0 \in D$ such that $s_\alpha \in f^{-1}(V)$ for all $\alpha \succeq \alpha_0$. Applying $f$, we obtain $f(s_\alpha) \in V$ for all $\alpha \succeq \alpha_0$. Since $V$ was an arbitrary open neighbourhood of $f(x)$, this shows $f(s_\alpha) \to f(x)$ in $(Y, \tau_Y)$. [guided] Assume $f$ is continuous and let $(s_\alpha)_{\alpha \in D}$ be a net in $X$ with $s_\alpha \to x$. We must show $f(s_\alpha) \to f(x)$ in $Y$. Let $V \in \tau_Y$ be any open neighbourhood of $f(x)$. By the definition of continuity, $f^{-1}(V) \in \tau_X$. Moreover, $x \in f^{-1}(V)$ since $f(x) \in V$. So $f^{-1}(V)$ is an open neighbourhood of $x$ in $X$. Since $s_\alpha \to x$, there exists $\alpha_0 \in D$ such that $s_\alpha \in f^{-1}(V)$ for all $\alpha \succeq \alpha_0$. Applying $f$ to both sides: $f(s_\alpha) \in V$ for all $\alpha \succeq \alpha_0$. Since $V$ was arbitrary, $f(s_\alpha) \to f(x)$. The argument is a direct translation: continuity gives us control of preimages, and net convergence translates that control into eventual membership. This is the net-theoretic analogue of the elementary sequence argument in metric spaces, but here no countability is needed. [/guided] [/step] [step:Prove the converse by contrapositive — build a net whose image fails to converge] We prove the contrapositive: assume $f$ is not continuous and produce a net $(s_\alpha)_{\alpha \in D}$ with $s_\alpha \to x$ but $f(s_\alpha) \not\to f(x)$. Since $f$ is not continuous, there exists $V \in \tau_Y$ such that $f^{-1}(V)$ is not open in $X$. The set $f^{-1}(V)$ is not open means there exists a point $x \in f^{-1}(V)$ such that no open neighbourhood of $x$ is contained in $f^{-1}(V)$. Equivalently, for every $U \in \tau_X$ with $x \in U$, the set $U \setminus f^{-1}(V)$ is non-empty. Define the directed set $D := \{U \in \tau_X : x \in U\}$, ordered by reverse inclusion ($U \preceq W$ iff $W \subset U$), as in the proof of the [Net Characterisation of Closure](/theorems/1045). For each $U \in D$, choose $s_U \in U \setminus f^{-1}(V)$. This defines a net $s: D \to X$, $U \mapsto s_U$. The net $(s_U)_{U \in D}$ converges to $x$: for any open neighbourhood $W$ of $x$, if $U \succeq W$ (i.e., $U \subset W$), then $s_U \in U \subset W$. However, $f(s_U) \notin V$ for every $U \in D$, since $s_U \notin f^{-1}(V)$. Thus $f(s_U)$ is not eventually in the open neighbourhood $V$ of $f(x)$, so $f(s_U) \not\to f(x)$. [guided] We prove the contrapositive: if $f$ is not continuous, then the net-convergence condition fails. The failure of continuity gives us a concrete open set to exploit. Since $f$ is not continuous, there exists $V \in \tau_Y$ with $f^{-1}(V) \notin \tau_X$. Since $f^{-1}(V)$ is not open, there exists $x \in f^{-1}(V)$ that is not an interior point: every open neighbourhood $U$ of $x$ contains a point outside $f^{-1}(V)$. That is, for every $U \in \tau_X$ with $x \in U$, the set $U \setminus f^{-1}(V) \neq \varnothing$. We build a net indexed by the neighbourhood system of $x$. Define $D := \{U \in \tau_X : x \in U\}$ with the reverse-inclusion order $U \preceq W$ iff $W \subset U$. As verified in the proof of the [Net Characterisation of Closure](/theorems/1045), $(D, \preceq)$ is a directed set. For each $U \in D$, select $s_U \in U \setminus f^{-1}(V)$ (possible since this set is non-empty). The resulting net $(s_U)_{U \in D}$ converges to $x$ by the same argument as before: any open neighbourhood $W$ of $x$ belongs to $D$, and $U \succeq W$ implies $s_U \in U \subset W$. Why does the image net fail to converge to $f(x)$? Because $s_U \notin f^{-1}(V)$ for every $U \in D$, which means $f(s_U) \notin V$ for every $U$. But $V$ is an open neighbourhood of $f(x)$ (since $x \in f^{-1}(V)$, i.e., $f(x) \in V$). The image net is never in $V$, so it cannot be eventually in $V$, and $f(s_U) \not\to f(x)$. This construction shows exactly where the converse argument requires the Axiom of Choice: we make one choice per neighbourhood of $x$. The forward direction, by contrast, is choice-free. [/guided] [/step]