Theorem nottru

A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.)

Conclusion
\( \vdash \neg \top \leftrightarrow \bot \)
Proof
df-fal
bicomi _