 Corollary 2.4 (Subformula property) If \(\cD\) is a cut-free proof of the sequent \(\Gamma\Rightarrow\Delta\), then all formulae in \(\cD\) are subformulae of elements in either \(\Gamma\) or \(\Delta\).