  Existential fixed point logic (EFPL) is a natural fit for some applications,
and the purpose of this talk is to attract attention to EFPL. The logic is also
interesting in its own right as it has attractive properties. One of those
properties is rather unusual: truth of formulas can be defined (given
appropriate syntactic apparatus) in the logic. We mentioned that property
elsewhere, and we use this opportunity to provide the proof.
