Solution (source code)

= Solution

A set $S$ is a <deductively closed set of formulae> when every consequence of $S$ already belongs to it:
$$
S\vdash\varphi\Longrightarrow\varphi\in S.
$$
It is a <consistent set of formulae> when it does not prove a contradiction,
$$
S\nvdash\bot.
$$

If $S$ is inconsistent, there is a formal derivation of $\bot$ from assumptions in $S$. By the <finite character of formal proofs>, that derivation mentions only finitely many assumptions $s_1,\ldots,s_m\in S$. Hence
$$
\{s_1,\ldots,s_m\}\vdash\bot,
$$
so this finite subset of $S$ is already inconsistent.