Proposition 25: Provided a variable x occurs in at least one of the statements \alpha, \beta, ..., \omega , it also occurs in the iterated disjunction (\alpha \vee \beta \vee \cdots \vee \omega).

Proof: We shall argue by means of structural induction over the definition of iterated disjunction.

Base cases: Suppose x occurs in at least one of \alpha , \beta and \gamma . Then, x occurs in at least one of \alpha or \beta , or else x occurs in \gamma . In the former case, x occurs in the disjunction (\alpha \vee \beta) by [12], so by the same result it occurs in \big( (\alpha \vee \beta) \vee \gamma) . In the latter case, x occurs in this same statement by the same rule. But this statement is the definition of (\alpha \vee \beta \vee \gamma) .

Inductive step: We take as the induction hypothesis that the desired result is known for statements \alpha, \beta, ..., \psi , and want to show from this that it is also justified for \alpha, \beta, ..., \psi, \omega . If x occurs in at least one of \alpha, \beta, ..., \psi, \omega , then it either occurs in at least one of \alpha, \beta, ..., \psi or it occurs in \omega . In the former case, x occurs in (\alpha \vee \beta \vee \cdots \vee \psi) by the induction hypothesis. Thus, in either of the cases, it occurs inn \big( (\alpha \vee \beta \vee \cdots \vee \psi) \vee \omega\big) by [12]. But this statement is the definition of (\alpha \vee \beta \vee \cdots \vee \psi \vee \omega) . \square