The theorem states that if a set of sentences of a first-order language $L$ is inconsistent, then some finite subset of it is inconsistent. Suppose $\Delta\subseteq L$ is inconsistent. Then by definition $\Delta\proves\perp$ , i.e. there is a formal proof of ``false'' using only assumptions from $\Delta$ . Formal proofs are finite objects, so let $\Gamma$ collect all the formulas of $\Delta$ that are used in the proof.