A map into a compact space whose graph is closed is continuous; so for a compact Hausdorff codomain, continuity and closedness of the graph are equivalent

Assume $Y$ is compact and $G_f$ is closed, and put $N := (X \times Y) \setminus G_f$, which is open.

Fix $x_0 \in X$ and an open $V \subseteq Y$ with $f(x_0) \in V$, and put $C := Y \setminus V$; then $C$ is closed in $Y$, hence a compact subspace.

Let $\mathcal{P}$ be the set of all pairs $(U, W)$ such that $U$ is open in $X$, $W$ is open in $Y$, $x_0 \in U$ and $(U \times W) \cap G_f = \varnothing$; this family is specified by a formula and nothing is selected in forming it.

If $Y$ is Hausdorff and $f$ is continuous then $G_f$ is closed, which is claim 2.

Every $y \in C$ lies in $W$ for some $(U,W) \in \mathcal{P}$: since $f(x_0) \in V$ and $y \notin V$ we have $y \ne f(x_0)$, so $(x_0, y) \in N$, and by [A1] there is a basic box $U \times W$ with $(x_0,y) \in U \times W \subseteq N$, which gives $(U,W) \in \mathcal{P}$.

The family $\mathcal{V} := \{\, W \cap C : (U,W) \in \mathcal{P} \text{ for some } U \,\}$ consists of sets open in the subspace $C$ and its union is $C$, by step 2.1.

By compactness of $C$ there is a finite subfamily of $\mathcal{V}$ whose union is $C$; being finite it may be listed as $V_0, \dots, V_{n-1}$ for some $n \in \mathbb{N}$, so that $C \subseteq \bigcup_{i<n} V_i$.

For each $i < n$ the set $\mathcal{P}_i := \{\, (U,W) \in \mathcal{P} : W \cap C = V_i \,\}$ is nonempty, since $V_i \in \mathcal{V}$; so by [L4] applied to the function $i \mapsto \mathcal{P}_i$ on $n$ there is a choice function on the family of these sets, and it supplies a pair $(U_i, W_i) \in \mathcal{P}_i$ for every $i < n$.

Put $U := \{\, x \in X : x \in U_i \text{ for every } i < n \,\}$; this is $X$ when $n = 0$ and a finite intersection of open sets otherwise, hence open in either case, and $x_0 \in U$ since $x_0 \in U_i$ for every $i < n$.

$f[U] \subseteq V$: let $x \in U$ and suppose $f(x) \notin V$, that is $f(x) \in C$; then $f(x) \in V_i = W_i \cap C \subseteq W_i$ for some $i < n$ by step 4.1, while $x \in U \subseteq U_i$, so the point $(x, f(x))$ of $G_f$ lies in $U_i \times W_i$, contradicting $(U_i \times W_i) \cap G_f = \varnothing$; hence $f(x) \in V$.

By steps 6.1 and 7.1 there is, for the arbitrary $x_0 \in X$ and the arbitrary open $V$ containing $f(x_0)$ fixed in step 1.2, an open $U \ni x_0$ with $f[U] \subseteq V$; so $f$ is continuous by [A2], which is claim 1.

If $Y$ is compact and Hausdorff then step 8.1 gives one implication and step 1.4 the other, so continuity of $f$ and closedness of $G_f$ are equivalent, which is claim 3; with steps 8.1 and 1.4 the theorem is proved.