\documentclass{article}
\usepackage{latexsym}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newenvironment{Proof}{\trivlist\item[\hskip\labelsep{\bf Proof}]}{\hfill$\Box$\par}
\begin{document}

\section{Wellfounded part}

Given a binary relation $<$ on a set $S$, the subset $W$ of $S$ called the
\textbf{wellfounded part} of $S$ w.r.t.\ $<$ is defined inductively as
follows:
\[ \frac{\forall y < x.~ y \in W}{x \in W} \]
The corresponding induction principle easily yields the principle of
\textbf{wellfounded part induction}:
\[ \frac{\forall x \in W.~(\forall y < x.~P(y)) \Rightarrow P(x)}{\forall x \in W.~ P(x)} \]
It also follows that $<$ is wellfounded iff $W = S$.

\section{The proof}

Let $<$ be a wellfounded relation on a set $A$, and let ${\cal M}(A)$ be the
set of all finite multisets over $A$. We use set-notation for multisets. The
letters $a$ and $b$ range over A; $K$, $M$ and $N$ range over ${\cal M}(A)$.
We define the following abbreviations:
\begin{eqnarray*}
M < a &\Leftrightarrow& \forall b \in M.~ b < a\\
N <_{mult} M &\Leftrightarrow&
  \exists M_0, a, K.~ M = M_0 \cup \{a\} \land N = M_0 \cup K \land K < a\\
W &=& \mbox{the wellfounded part of ${\cal M}(A)$ w.r.t.\ $<_{mult}$}
\end{eqnarray*}

\begin{lemma}\label{lemma1}
  If $\forall b<a.~\forall M \in W.~ M \cup \{b\} \in W$ and $M_0 \in W$ and
  $\forall M <_{mult} M_0.~ M \cup \{a\} \in W$ then $M_0 \cup \{a\} \in W$.
\end{lemma}
\begin{Proof}
by definition of $W$. Let $N <_{mult} M_0 \cup \{a\}$. We need to prove $N
\in W$. There are two possibilities why $N <_{mult} M_0 \cup \{a\}$ holds:
\begin{itemize}
\item If $N = M \cup \{a\}$ for some $M <_{mult} M_0$ then $N \in W$ follows
  from the third assumption.
\item If $N = M_0 \cup K$ for some $K < a$ then $N \in W$ follows
  from the first two assumptions by induction on the size of $K$.
\end{itemize}
\end{Proof}

\begin{lemma}\label{lemma2}
  If $\forall b<a.~\forall M \in W.~ M \cup \{b\} \in W$ then $\forall M \in
  W.~ M \cup \{a\} \in W$.
\end{lemma}
\begin{Proof} From Lemma~\ref{lemma1} by wellfounded part induction.
\end{Proof}

\begin{lemma}\label{lemma3}
  $\forall M \in W.~ M \cup \{a\} \in W$.
\end{lemma}
\begin{Proof} From Lemma~\ref{lemma2} by wellfounded induction on $a$.
\end{Proof}

\begin{theorem}
  $M \in W$.
\end{theorem}
\begin{Proof}
  by induction on the size of $M$. The base case $\emptyset \in W$ holds
  because there is no $N <_{mult} \emptyset$. Lemma~\ref{lemma3} covers the
  induction step.
\end{Proof}
\bigskip

\noindent
Thus we know that $<_{mult}$ is wellfounded on all of ${\cal M}(A)$.

\end{document}
