Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma

Suppose $(X, \mathcal{T})$ is not compact. Then $X \ne \varnothing$, the empty space being compact by [L1], and the family $\mathcal{P}$ of those open covers of $X$ that have no finite subcover is a nonempty subfamily of the power set of $\mathcal{T}$, partially ordered by inclusion.

Every chain $\mathcal{C} \subseteq \mathcal{P}$ has an upper bound in $\mathcal{P}$. For $\mathcal{C} = \varnothing$ any member of $\mathcal{P}$ is an upper bound, and $\mathcal{P}$ is nonempty by step 1.1. For $\mathcal{C} \ne \varnothing$ take $\mathcal{B} := \bigcup \mathcal{C}$, a family of open sets whose union is $X$ because the union of any one member of $\mathcal{C}$ already is; were $\mathcal{B}$ to have a finite subcover $U_0, \dots, U_n$, then for each $j \le n$ the set of members of $\mathcal{C}$ containing $U_j$ is nonempty, [L4] would supply $\mathcal{D}_0, \dots, \mathcal{D}_n \in \mathcal{C}$ with $U_j \in \mathcal{D}_j$, and [L3] would put all of them inside one $\mathcal{D} \in \mathcal{C}$, which would then have the finite subcover $U_0, \dots, U_n$ and could not lie in $\mathcal{P}$. So $\mathcal{B} \in \mathcal{P}$, and it contains every member of $\mathcal{C}$.

By [L6] the poset $\mathcal{P}$ has a maximal element $\mathcal{M}$: an open cover of $X$ with no finite subcover such that the only member of $\mathcal{P}$ containing it is itself.

For every open $U \notin \mathcal{M}$ there is a finite $\mathcal{F} \subseteq \mathcal{M}$ with $X = U \cup \bigcup \mathcal{F}$. Indeed $\mathcal{M} \cup \{U\}$ is an open cover strictly containing $\mathcal{M}$, so by maximality it is not in $\mathcal{P}$ and has a finite subcover; that subcover must contain $U$, since otherwise it would be a finite subcover of $\mathcal{M}$ itself, and the members other than $U$ form the required finite $\mathcal{F} \subseteq \mathcal{M}$.

Let $x \in X$. Since $\mathcal{M}$ covers $X$ there is $M \in \mathcal{M}$ with $x \in M$, and by [L7] there are $m \in \mathbb{N}$ and $S_0, \dots, S_m \in \mathcal{S}$ with $x \in S_0 \cap \dots \cap S_m \subseteq M$; the remaining alternative of [L7], that no member of $\mathcal{S}$ is taken and the basic set is $X$ itself, would give $X \subseteq M$ and so make $\{M\}$ a finite subcover of $\mathcal{M}$, which step 3.1 forbids.

Some $S_j$ lies in $\mathcal{M}$. For if none did, then by step 4.1 the set of finite $\mathcal{F} \subseteq \mathcal{M}$ with $X = S_j \cup \bigcup \mathcal{F}$ is nonempty for each $j \le m$, so [L4] supplies $\mathcal{F}_0, \dots, \mathcal{F}_m$; every $y \in X$ either lies in $S_0 \cap \dots \cap S_m$ or fails to lie in some $S_j$ and then lies in $\bigcup \mathcal{F}_j$, so $X = (S_0 \cap \dots \cap S_m) \cup \bigcup \mathcal{F}_0 \cup \dots \cup \bigcup \mathcal{F}_m \subseteq M \cup \bigcup \mathcal{F}_0 \cup \dots \cup \bigcup \mathcal{F}_m$, exhibiting a finite subfamily of $\mathcal{M}$ with union $X$ — a union of finitely many listable families being listed by concatenation — which step 3.1 forbids.

Hence $\mathcal{S} \cap \mathcal{M}$ covers $X$: every $x \in X$ lies in some $S_j$ of step 4.2 that belongs to $\mathcal{M}$ by step 5.1, and $x \in S_0 \cap \dots \cap S_m \subseteq S_j$.

By [A1] the cover $\mathcal{S} \cap \mathcal{M}$ of $X$ by members of $\mathcal{S}$ has a finite subfamily with union $X$; that subfamily is a finite subfamily of $\mathcal{M}$ with union $X$, contradicting the choice of $\mathcal{M}$ at step 3.1. So the supposition of step 1.1 is untenable and $(X, \mathcal{T})$ is compact.