First, let $\tau$ be an atomic sentence. Then, $\tau=t<u$ or $\tau=t=u$ where $t$ and $u$ are variable-free terms. But then, according to Lemma 33B, there are $m$ and $n$ such that $A_{E}\vdash t=\mathbb{S}^{m}0$ and $A_{E}\vdash u=\mathbb{S}^{n}0$ . Further, $A_{E}\vdash\mathbb{S}^{m}0=\mathbb{S}^{n}0$ iff $m=n$ and $A_{E}\vdash\mathbb{S}^{m}0\neq\mathbb{S}^{n}0$ iff $m\neq n$ (by S1 and S2), and, using this, by Lemma 33A, $A_{E}\vdash\mathbb{S}^{m}0<\mathbb{S}^{n}0$ iff $m<n$ and $A_{E}\vdash\mathbb{S}^{m}0\nless\mathbb{S}^{n}0$ iff $m\ge n$ . Using these facts, we can show that $A_{E}\vdash t<u$ iff $m<n$ and $A_{E}\vdash\neg t<u$ iff $m\ge n$ , and $A_{E}\vdash t=u$ iff $m=n$ and $A_{E}\vdash\neg t=u$ iff $m\neq n$ . For example, for $m<n$ , $A_{E}\vdash\forall x\forall y\forall z(x=y\rightarrow x<z\rightarrow y<z)$ and $A_{E}\vdash\forall x\forall y\forall z(x=y\rightarrow z<x\rightarrow z<y)$ (deduction axiom group 6, DA6), and using DA2, we can deduce $A_{E}\vdash\mathbb{S}^{m}0=t\rightarrow\mathbb{S}^{m}0<\mathbb{S}^{n}0\rightarrow t<\mathbb{S}^{n}0$ and $A_{E}\vdash\mathbb{S}^{n}0=u\rightarrow t<\mathbb{S}^{n}0\rightarrow t<u$ , and, similarly for $A_{E}\vdash\neg u=t$ and $A_{E}\vdash\neg u<t$ .

Second, let $\tau$ be a sentence of the form $\neg\tau_{1}$ or $\tau_{2}\rightarrow\tau_{3}$ true in $\mathfrak{A}$ , where $\tau_{i}$ is such that $A_{E}\vdash\tau_{i}$ iff $\tau_{i}$ is true in $\mathfrak{A}$ , and $A_{E}\vdash\neg\tau_{i}$ iff $\tau_{i}$ is false in $\mathfrak{A}$ . We show that the same applies to $\tau$ . Indeed, if $\tau$ is true in $\mathfrak{A}$ , then, respectively, $\tau_{1}$ is false in $\mathfrak{A}$ , and $\tau_{2}$ is false or $\tau_{3}$ is true in $\mathfrak{A}$ , implying $A_{E}\vdash\neg\tau_{1}$ , and $A_{E}\vdash\neg\tau_{2}\vee\tau_{3}$ , i.e. $A_{E}\vdash\tau$ , otherwise $\tau_{1}$ is true in $\mathfrak{A}$ , and $\tau_{2}$ is true, $\tau_{3}$ is false in $\mathfrak{A}$ , implying $A_{E}\vdash\neg\neg\tau_{1}$ , and $A_{E}\vdash\neg(\neg\tau_{2}\vee\tau_{3})$ , i.e. $A_{E}\vdash\neg\tau$ .