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\mathrm{\ne }\mathrm{\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}=\mathrm{\varnothing }$ any member of $\mathcal{P}$ is an upper bound, and $\mathcal{P}$ is nonempty by step 1.1. For $\mathcal{C}\mathrm{\ne }\mathrm{\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\mathrm{\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 \cdots \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 \cdots \cap S_m$ or fails to lie in some $S_j$ and then lies in $\bigcup {\mathcal{F}}_j$, so $X=(S_0\cap \cdots \cap S_m)\cup \bigcup {\mathcal{F}}_0\cup \cdots \cup \bigcup {\mathcal{F}}_m\subseteq M\cup \bigcup {\mathcal{F}}_0\cup \cdots \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 \cdots \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.