Branch of Finite Propositional Tableau is Finite

Theorem

Let $T$ be a finite propositional tableau.

Let $\Gamma$ be a branch of $T$.

Then $\Gamma$ is a finite branch.

Proof

By definition, a finite propositional tableau $T$ is formed by applying the tableau extension rules a finite number of times.

Each tableau extension rule extends $T$ finitely.

Therefore $T$ is a finite tree.

The result follows from Branch of Finite Tree is Finite.

$\blacksquare$