Assume that \Gamma \nvdash \alpha \mathbin: \varphi. By Lemma 2.13 the set \Gamma_0 =\Gamma,\alpha \mathbin: \lnot \varphi is consistent. We will extend it to a maximal consistent saturated set \Gamma^\ast. By applying the previous lemma we may assume that there are infinitely many atomic labels that are not mentioned in \Gamma_0.
We construct \Gamma^\ast as the union of \Gamma_n where each \Gamma_n is a finite extension of \Gamma_0. First, we enumerate all labelled formulas and when constructing \Gamma_{n+1} we pick the nth labelled formula \beta \mathbin: \psi and add either \beta \mathbin:\psi or \beta \mathbin:\lnot\psi. By Proposition 3.2 one of these is consistent with \Gamma_n.
By Proposition 3.3 we can assure that if we add a labelled formula \beta \mathbin: \sigma \mathrel{\vphantom{\lor}\mathpalette\ilor@\relax} \theta then we also add p\mathbin: \sigma, q\mathbin:
\theta and \beta = p + q for some new atomic labels p and q, and keeping \Gamma_{n+1} consistent. This construction assures that \Gamma^\ast is maximal consistent and saturated.
Now, let T=\set{\alpha | \alpha \mathbin: \mathord{\vphantom{\top}\mathpalette\itop@\relax} \in \Gamma^\ast}. Let B be the Lindenbaum–Tarski Boolean algebra of labels over T, i.e., its elements are equivalence classes of labels under the relation of T-provable equivalence:
B = \ensuremath{\mathtt{Lb}} / \mathord\sim_T = \set{[\alpha]_T | \alpha \in \ensuremath{\mathtt{Lb}}},
where \alpha \sim_T b iff T \vdash \alpha \leftrightarrow \beta (in classical propositional logic) and [\alpha]_T=\set{\beta \in \ensuremath{\mathtt{Lb}} | \alpha \sim_T \beta}. Observe that B is the trivial one-element Boolean algebra iff T is the inconsistent theory, i.e., iff 0 \in T. Define the homomorphisms h: \ensuremath{\mathtt{Lb}} \to B and H: \ensuremath{\mathtt{Fm}} \to {\mathcal P} B by
\begin{gathered}
h(p_i)=[p_i]_T \in B \text{ for atomic labels $p_i$, and}\\ H(P_i) = \set{h(\alpha) |
\alpha\mathbin: P_i \in\Gamma^\ast} \text{ for atomic formulas $P_i$}.
\end{gathered}
Claim. h(\alpha) \in H(\varphi) iff \alpha \mathbin: \varphi \in \Gamma^\ast.
The claim is proved by induction on formulas. The base case follows immediately from the definition of H and the observation that
H(\mathord{\vphantom{\bot}\mathpalette\ibot@\relax}) =
\{[0]_T\}.
This is seen by taking h(\beta) \in H(\mathord{\vphantom{\bot}\mathpalette\ibot@\relax}) and observing that \beta \mathbin: \mathord{\vphantom{\bot}\mathpalette\ibot@\relax}
\in \Gamma^\ast and so - \beta \mathbin: \mathord{\vphantom{\top}\mathpalette\itop@\relax}
\in \Gamma^\ast and, thus, - \beta \in T and \beta \in [0]_T.
If \varphi is \psi \lor \sigma, \psi \land \sigma or \lnot \psi the induction step is straightforward, as for example \alpha \mathbin: \psi \land
\sigma \in \Gamma^\ast iff \alpha \mathbin: \psi \in \Gamma^\ast and \alpha \mathbin: \sigma
\in \Gamma^\ast and, by the induction hypothesis, this is equivalent to h(\alpha ) \in H(\psi) and h(\alpha ) \in H(\sigma), i.e., h(\alpha ) \in H(\psi) \cap
H(\sigma) = H(\psi\land \sigma).
For the case when \varphi is \mathord{\vphantom{\lnot}\mathpalette\ilnot@\relax} \psi note that \alpha \mathbin: \mathord{\vphantom{\lnot}\mathpalette\ilnot@\relax} \psi
\in \Gamma^\ast iff - \alpha \mathbin: \psi \in \Gamma^\ast iff h(- \alpha )
\in H(\psi) iff - h(\alpha ) \in H(\psi) iff h(\alpha) \in H(\mathord{\vphantom{\lnot}\mathpalette\ilnot@\relax} \psi).
When \varphi is \psi \mathrel{\vphantom{\lor}\mathpalette\ilor@\relax} \sigma note that \alpha \mathbin: \psi \mathrel{\vphantom{\lor}\mathpalette\ilor@\relax} \sigma \in
\Gamma^\ast iff there are labels \beta_1 and \beta_2 such that \beta_1 \mathbin: \psi \in
\Gamma^\ast, \beta_2\mathbin: \sigma \in \Gamma^\ast and \alpha = \beta_1 +
\beta_2 \in \Gamma^\ast. By the induction hypothesis this is equivalent to h(\beta_1) \in H(\psi), h(\beta_2) \in H(\sigma) and h(\alpha) = h(\beta_1+
\beta_2) = h(\beta_1) + h(\beta_2). Thus this is equivalent to h(\alpha) \in H(\psi \mathrel{\vphantom{\lor}\mathpalette\ilor@\relax}
\sigma).
The case when \varphi is \psi \mathrel{\vphantom{\land}\mathpalette\iland@\relax} \sigma is treated similarly, ending the proof of the claim.
It now follows immediately that for these choices of B, H, and h we have h(\alpha) \in H(\varphi) for all \alpha \mathbin:\varphi \in
\Gamma_0 and thus \Gamma \nvDash \alpha \mathbin:\varphi.