Two self-implications (see id) are equivalent. This theorem, rather trivial in our axiomatization, is (the biconditional form of) a standard axiom for monothetic BCI logic. This is the most general theorem of which trujust is an instance. Relatedly, this would be the justification theorem if the definition of T. were dftru2. (Contributed by BJ, 7-Sep-2022.)