%
\label{lem:membership-wf}
Define the \textbf{strict membership} relation by:
\[
    \underline{a} \in_\tau^\circ \underline{b}
    \quad:\iff\quad
    \underline{a} \in_\tau \underline{b}
    \;\text{ and }\;
    \underline{a} \neq \underline{b}.
\]
Equivalently,
$\underline{a} \in_\tau^\circ \underline{b}$
iff $\underline{a}$ is a \emph{proper} divisor of $\underline{b}$.
Then $\in_\tau^\circ$ is \textbf{well-founded}:
there are no infinite strictly descending chains
$\cdots \in_\tau^\circ \underline{x}_2
\in_\tau^\circ \underline{x}_1
\in_\tau^\circ \underline{x}_0$.

If $\underline{a} \in_\tau^\circ \underline{b}$,
then $\underline{a} \mid \underline{b}$
and $\underline{a} \neq \underline{b}$.
By properties of divisibility in $\mathbb{N}$,
this implies $\underline{a} < \underline{b}$
(in the natural number ordering).
Thus, any descending chain under $\in_\tau^\circ$
corresponds to a strictly decreasing sequence of natural numbers.
Since $\mathbb{N}$ is well-ordered,
such a sequence cannot be infinite.