[proofplan] For the forward direction, we use the [Ultrafilter Characterisation of Compactness](/theorems/1049) together with the [Net-Filter Correspondence](/theorems/1050): given any net, its eventuality filter is contained in an ultrafilter, which converges by compactness, yielding a cluster point. For the converse, we show that if every net has a cluster point, then the finite intersection property (FIP) holds for all families of closed sets, which is equivalent to compactness. [/proofplan] [step:Show that compactness implies every net has a cluster point] Assume $(X, \tau)$ is compact. Let $(s_\alpha)_{\alpha \in D}$ be a net in $X$. By the [Net-Filter Correspondence](/theorems/1050) (Part 1), the eventuality filter $\mathcal{F}_s$ is a filter on $X$. By Zorn's Lemma, there exists an ultrafilter $\mathcal{U}$ on $X$ with $\mathcal{F}_s \subset \mathcal{U}$. By the [Ultrafilter Characterisation of Compactness](/theorems/1049), $\mathcal{U}$ converges to some $x \in X$: every open neighbourhood $U$ of $x$ satisfies $U \in \mathcal{U}$. We show $x$ is a cluster point of $(s_\alpha)$. Let $U$ be an open neighbourhood of $x$ and let $\alpha_0 \in D$. The tail set $T_{\alpha_0} := \{s_\alpha : \alpha \succeq \alpha_0\}$ belongs to $\mathcal{F}_s \subset \mathcal{U}$, and $U \in \mathcal{U}$. Since $\mathcal{U}$ is a filter, $T_{\alpha_0} \cap U \in \mathcal{U}$, and in particular $T_{\alpha_0} \cap U \neq \varnothing$ (since $\varnothing \notin \mathcal{U}$). So there exists $\alpha \succeq \alpha_0$ with $s_\alpha \in U$. [guided] Assume $(X, \tau)$ is compact and let $(s_\alpha)_{\alpha \in D}$ be a net in $X$. The strategy is to lift the problem to filters, apply the ultrafilter characterisation, and then translate back. **Lift to filters.** By the [Net-Filter Correspondence](/theorems/1050) (Part 1), the eventuality filter $\mathcal{F}_s = \{A \subset X : s_\alpha \in A \text{ eventually}\}$ is a proper filter on $X$. **Extend to an ultrafilter.** By Zorn's Lemma, extend $\mathcal{F}_s$ to an ultrafilter $\mathcal{U} \supset \mathcal{F}_s$. The poset of proper filters containing $\mathcal{F}_s$, ordered by inclusion, is non-empty (it contains $\mathcal{F}_s$) and closed under chain unions, so Zorn's Lemma applies. **Apply the ultrafilter characterisation.** Since $X$ is compact, the [Ultrafilter Characterisation of Compactness](/theorems/1049) guarantees that $\mathcal{U}$ converges to some $x \in X$. **Translate back to the net.** We claim $x$ is a cluster point of $(s_\alpha)$. Let $U$ be an open neighbourhood of $x$ and $\alpha_0 \in D$. We need $\alpha \succeq \alpha_0$ with $s_\alpha \in U$. Since $\mathcal{U}$ converges to $x$, $U \in \mathcal{U}$. The tail set $T_{\alpha_0} = \{s_\alpha : \alpha \succeq \alpha_0\} \in \mathcal{F}_s \subset \mathcal{U}$. Filters are closed under finite intersections, so $T_{\alpha_0} \cap U \in \mathcal{U}$. Since $\varnothing \notin \mathcal{U}$, we get $T_{\alpha_0} \cap U \neq \varnothing$, yielding the required $\alpha$. Note that we could alternatively prove this step directly without filters, by using the FIP. But routing through ultrafilters makes the argument cleaner and also demonstrates the power of the net-filter correspondence. [/guided] [/step] [step:Show that the cluster point property implies compactness via the finite intersection property] We prove the contrapositive: if $X$ is not compact, then some net in $X$ has no cluster point. Since $X$ is not compact, there exists an open cover $\{V_i\}_{i \in I}$ with no finite subcover. The family of closed complements $\{C_i\}_{i \in I}$, where $C_i := X \setminus V_i$, has the finite intersection property: for every finite $J \subset I$, \begin{align*} \bigcap_{j \in J} C_j = X \setminus \bigcup_{j \in J} V_j \neq \varnothing. \end{align*} Define the directed set $D$ consisting of all non-empty finite subsets of $I$, ordered by inclusion: $J_1 \preceq J_2$ iff $J_1 \subset J_2$. This is directed since $J_1 \cup J_2$ is an upper bound for $J_1$ and $J_2$. For each $J \in D$, the FIP guarantees $\bigcap_{j \in J} C_j \neq \varnothing$. Choose $s_J \in \bigcap_{j \in J} C_j$. This defines a net $(s_J)_{J \in D}$ in $X$. We show this net has no cluster point. Let $x \in X$. Since $\{V_i\}_{i \in I}$ covers $X$, there exists $i_0 \in I$ with $x \in V_{i_0}$. Consider the finite set $J_0 := \{i_0\} \in D$. For every $J \succeq J_0$ (i.e., $J \supset \{i_0\}$), we have $s_J \in \bigcap_{j \in J} C_j \subset C_{i_0} = X \setminus V_{i_0}$. So $s_J \notin V_{i_0}$ for all $J \succeq J_0$, meaning the net is eventually outside the open neighbourhood $V_{i_0}$ of $x$. In particular, $x$ is not a cluster point: the net is not frequently in $V_{i_0}$, since it is eventually outside $V_{i_0}$. [guided] We prove the contrapositive: if $X$ is not compact, we build a net with no cluster point. **Extract the FIP family.** Take an open cover $\{V_i\}_{i \in I}$ with no finite subcover. The closed complements $C_i = X \setminus V_i$ satisfy the FIP, as established in the proof of the [Ultrafilter Characterisation of Compactness](/theorems/1049). **Build the net.** The directed set $D$ is the collection of all non-empty finite subsets of $I$, ordered by inclusion. For each $J \in D$, select $s_J \in \bigcap_{j \in J} C_j$ (possible by the FIP). The resulting net $(s_J)_{J \in D}$ has a crucial monotonicity property: as $J$ grows (more indices are included), $s_J$ is forced into progressively smaller intersections of closed sets. **Show no cluster point exists.** For any $x \in X$, pick $i_0$ with $x \in V_{i_0}$. The tail past $J_0 = \{i_0\}$ consists of all $J \supset \{i_0\}$, and every such $s_J$ belongs to $C_{i_0} = X \setminus V_{i_0}$. So the net is eventually outside $V_{i_0}$, which means it cannot be frequently in $V_{i_0}$. Since $V_{i_0}$ is an open neighbourhood of $x$ that the net eventually avoids, $x$ is not a cluster point. The argument is constructive modulo the Axiom of Choice (used to select one point from each non-empty finite intersection). The directed set $D$ of finite subsets captures the essence of the FIP: it forces the net to "sample" deeper and deeper intersections, and the fact that these intersections have total intersection contained in $\bigcap_{i \in I} C_i = X \setminus \bigcup_{i \in I} V_i = \varnothing$ ensures that no point can remain a cluster point. [/guided] [/step] [step:Derive the equivalent subnet formulation] The equivalence "every net has a cluster point if and only if every net has a convergent subnet" follows from the [Cluster Points and Subnets](/theorems/1048) theorem, which establishes that $x$ is a cluster point of a net if and only if some subnet converges to $x$. Applying this equivalence, "every net has a cluster point" becomes "every net has a convergent subnet." [/step]