Theorem extru

There exists a variable such that \( \top \) holds; that is, there exists a variable. This corresponds under the standard translation to one of the formulations of the modal axiom (D), the other being 19.2. (Contributed by Anthony Hart, 13-Sep-2011.) (Proof shortened by BJ, 12-May-2019.)

Conclusion
\( \vdash \exists x \, \top \)
Proof
tru
exgen _