Description: Definition of the truth
value "true", or "verum", denoted by .
This is a tautology, as proved by tru1357. In this definition, biid230
is
used as the definiens, although any tautology, such as an axiom, can be
used in its place. This definition should be referenced directly only by
tru1357, and other proofs should depend on tru1357
(directly or indirectly)
instead of this definition, since there are many alternative ways to
define . (Contributed by Anthony Hart,
13-Oct-2010.)
(New usage is discouraged.)