\begin{definition}[Definition:Gentzen Proof System/Instance 1/Beta-Rule]
Let $\LL$ be the language of propositional logic.
Let $\mathscr G$ be instance 1 of a Gentzen proof system.
The '''$\beta$-rule''' allows for introducing a $\beta$-formula in the conclusion.
Its precise formulations is as follows:
$(\beta)$: For any $\beta$-formula $\mathbf B$ and associated $\mathbf B_1, \mathbf B_2$ from the table of $\beta$-formulas:
:: Given $U_1 \cup \set {\mathbf B_1, \mathbf B_2}$, one may infer $U_1 \cup \set {\mathbf B}$.
\end{definition}