|Description: Definition of the truth
value "true", or "verum", denoted by ⊤.
In this definition, an instance of id 22 is used as the definiens,
although any tautology, such as an axiom, can be used in its place.
This particular instance of id 22 was chosen so this definition can be
checked by the same algorithm that is used for predicate calculus. This
definition should be referenced directly only by tru 1642,
proofs should use tru 1642 instead of this definition, since there are
alternate ways to define ⊤. (Contributed
by Anthony Hart,
13-Oct-2010.) (Revised by NM, 11-Jul-2019.) Use tru 1642
(New usage is discouraged.)|