Solution (source code)

= Solution

Use the strict-order convention appropriate to the membership relation. A bounded <logical formula> is
$$
\begin{aligned}
TO(x)\ \equiv\;&(\forall u\in x)\,\neg(u\in u)\\
&\wedge(\forall u\in x)(\forall v\in x)(\forall w\in x)
\bigl((u\in v\wedge v\in w)\to u\in w\bigr)\\
&\wedge(\forall u\in x)(\forall v\in x)
\bigl(u=v\vee u\in v\vee v\in u\bigr).
\end{aligned}
$$
The first clause is irreflexivity, the second transitivity, and the third comparability of distinct elements. Irreflexivity and transitivity exclude $u\in v\in u$, so distinct elements cannot be ordered in both directions. These are exactly the axioms of a <strict total order> on the <set> $x$, with $\in$ as its order relation.

Every displayed <quantifier> is bounded by $x$, so \b[$TO(x)$ is $\Sigma_0$]. The <logical formula> does not assert that $x$ is transitive as a <set>, and no such additional assertion is needed to say that the restriction of membership to $x$ is a <total order>.