普遍ネット

$B\subseteq Y$ を任意にとる。$(x_d)$ の普遍性を $f^{-1}(B)\subseteq X$ に適用すると、$(x_d)$ は最終的に $f^{-1}(B)$ に入るか、最終的に $X\setminus f^{-1}(B)=f^{-1}(Y\setminus B)$ に入る。前者なら $(f(x_d))$ は最終的に $B$ に入り、後者なら最終的に $Y\setminus B$ に入る。よって像ネットは普遍である。

ネットを $(x_d)_{d\in D}$ とし、これが最終的に入る部分集合全体を
$$ \mathcal F_0:=\{A\subseteq X\mid (x_d)\text{ は最終的に }A\text{ に入る}\} $$
とおく。$X\in\mathcal F_0$、$\emptyset\notin\mathcal F_0$ であり、最終的に $A$ と $B$ に入るなら有向性により最終的に $A\cap B$ に入る。また $A\subseteq B$ なら、最終的に $A$ に入ることから最終的に $B$ に入る。よって $\mathcal F_0$ はフィルターである。
超フィルター補題により、$\mathcal F_0$ を含む超フィルター $\mathcal U$ をとる。任意の $A\in\mathcal U$ に対し、元のネットは頻繁に $A$ に入る。実際、そうでなければある $d_0$ 以降は $A$ に入らず、$X\setminus A\in\mathcal F_0\subseteq\mathcal U$ となる。すると $A$ と $X\setminus A$ の共通部分である空集合が $\mathcal U$ に属して矛盾する。
$$ E:=\{(d,A)\in D\times\mathcal U\mid x_d\in A\} $$
とおき、
$$ (d,A)\leq(e,B)\quad\Longleftrightarrow\quad d\leq e\text{ かつ }A\supseteq B $$
で順序づける。$E$ は空でない。さらに $(d_1,A_1),(d_2,A_2)\in E$ に対し、$d_3\geq d_1,d_2$ をとる。$A_1\cap A_2\in\mathcal U$ であり、元のネットは頻繁にそこへ入るので、ある $e\geq d_3$ が $x_e\in A_1\cap A_2$ を満たす。すると $(e,A_1\cap A_2)$ は両者の上界である。よって $E$ は有向集合である。
$\varphi\colon E\to D$ を $\varphi(d,A)=d$ とする。これは単調である。また任意の $d_0\in D$ に対し $(d_0,X)\in E$ であり、$(d,A)\geq(d_0,X)$ なら $\varphi(d,A)=d\geq d_0$ だから、$\varphi$ は共終である。したがって $(x_{\varphi(e)})_{e\in E}$ は元のネットの部分ネットである。
最後に $B\subseteq X$ をとる。超フィルターの二者択一性より $B\in\mathcal U$ または $X\setminus B\in\mathcal U$ である。$B\in\mathcal U$ の場合、頻繁性から $x_{d_0}\in B$ となる $d_0$ をとれば $(d_0,B)\in E$ であり、$(d,A)\geq(d_0,B)$ なら $A\subseteq B$ なので $x_d\in B$ である。ゆえに部分ネットは最終的に $B$ に入る。補集合が $\mathcal U$ に属する場合も同様である。したがってこの部分ネットは普遍である。

収束点が集積点であることは定義から従う。逆に $x$ を集積点とし、$V$ を $x$ の任意の近傍とする。普遍性により、$(x_d)$ は最終的に $V$ に入るか、最終的に $X\setminus V$ に入る。後者ならネットは頻繁に $V$ に入らず、$x$ が集積点であることに反する。したがって最終的に $V$ に入る。すべての近傍 $V$ についてこれが成り立つので $x_d\to x$ である。

(1 ⇒ 2) コンパクト空間では任意のネットが集積点を持つ（ネットの「コンパクト性のネットによる特徴づけ」）。普遍ネットに対してその集積点 $x$ をとれば、prop-universal-net-cluster-limit によりネットは $x$ に収束する。
(2 ⇒ 1) $X$ 上の任意のネットをとる。thm-universal-subnet-existence により普遍部分ネットを持ち、仮定によりその普遍部分ネットは収束する。よって任意のネットが収束部分ネットを持つ。再びネットの特徴づけにより $X$ はコンパクトである。

$X$ 上の普遍ネット $(x_d)_{d\in D}$ をとる。各射影 $\pi_i\colon X\to X_i$ に対し、prop-universal-net-image により $(\pi_i(x_d))_{d\in D}$ は $X_i$ 上の普遍ネットである。$X_i$ はコンパクトだから、thm-universal-net-compactness により、ある $y_i\in X_i$ に収束する。$y=(y_i)_{i\in I}\in X$ とおく。
直積位相でのネットの収束は座標ごとの収束と同値である。実際、$y$ の基本近傍は有限個の座標 $i\in F$ だけを制限する。各 $i\in F$ で $\pi_i(x_d)\to y_i$ となる添字の下限を有向性で同時に上回れば、それ以降の $x_d$ はその基本近傍に入る。したがって $x_d\to y$ である。
以上より $X$ 上のすべての普遍ネットは収束するから、thm-universal-net-compactness により $X$ はコンパクトである。なお、普遍部分ネットの存在で超フィルター補題を使っており、選択原理への依存が消えたわけではない。