diff --git a/sections/fin-dim-simple.tex b/sections/fin-dim-simple.tex
@@ -672,12 +672,12 @@ section.
It is already clear from the previous discussion that if \(\lambda\) is the
highest weight of \(M\) then \(\lambda(H_\alpha) \ge 0\) for all positive roots
-\(\alpha\). In other words, having \(\lambda(H_\alpha) \ge 0\), for all
-\(\alpha \in \Delta^+\), is a necessary condition for the existence of a simple
-\(\mathfrak{g}\)-module with highest weight given by \(\lambda\). Surprisingly,
-this condition is also sufficient. In other words\dots
+\(\alpha\). Indeed, as in the \(\mathfrak{sl}_3(K)\), for each \(\alpha \in
+\Delta^+\) we know \(\lambda(H_\alpha)\) is the highest eigenvalue of the
+action of \(h\) in the \(\mathfrak{sl}_2(K)\)-module \(\bigoplus_k M_{\lambda -
+k \alpha}\) -- which must be a non-negative integer. This fact may be
+summarized in the following proposition.
-% TODO: Move this definition to beforehand
\begin{definition}\index{weights!dominant weight}\index{weights!integral weight}
An element \(\lambda\) of \(P\) such that \(\lambda(H_\alpha) \ge 0\) for all
\(\alpha \in \Delta^+\) is referred to as an \emph{dominant integral weight
@@ -685,6 +685,17 @@ this condition is also sufficient. In other words\dots
\(P^+\).
\end{definition}
+\begin{proposition}\label{thm:highes-weight-of-fin-dim-is-dominant}
+ Suppose \(M\) is a finite-dimensional simple \(\mathfrak{g}\)-module and
+ \(\lambda\) is its highest weight. Then \(\lambda\) is a dominant integral
+ weight of \(\mathfrak{g}\).
+\end{proposition}
+
+The condition that \(\lambda \in P^+\) is thus necessary for the existence of a
+simple \(\mathfrak{g}\)-module with highest weight given by \(\lambda\). Given
+our previous experience with \(\mathfrak{sl}_2(K)\) and \(\mathfrak{sl}_3(K)\),
+it is perhaps unsurprising that this condition is also sufficient.
+
\begin{theorem}\label{thm:dominant-weight-theo}\index{weights!Highest Weight Theorem}
For each dominant integral \(\lambda \in P^+\) there exists precisely one
finite-dimensional simple \(\mathfrak{g}\)-module \(M\) whose highest weight
@@ -1095,14 +1106,13 @@ instance, consider\dots
\end{example}
While \(L(\lambda)\) is always a highest weight module of highest weight
-\(\lambda\), one can show that if \(\lambda \notin P^+\) then \(L(\lambda)\) is
-infinite-dimensional. Indeed, since the highest weight of a finite-dimensional
-simple \(\mathfrak{g}\)-module is always dominant integral, \(L(\lambda)\) is
-infinite-dimensional for any \(\lambda \notin P^+\). If \(\lambda = k_1 \beta_1
-+ \cdots + k_r \beta_r \in P\) is integral and \(k_i < 0\) for all \(i\), then
-\(M(\lambda) \cong L(\lambda)\) as in Example~\ref{ex:antidominant-verma}.
-
-Verma modules can thus serve as examples of infinite-dimensional simple
-modules. In the next chapter we expand our previous results by exploring the
-question: what are \emph{all} the infinite-dimensional simple
-\(\mathfrak{g}\)-modules?
+\(\lambda\), we can easily see that if \(\lambda \notin P^+\) then
+\(L(\lambda)\) is infinite-dimensional. Indeed, this is precisely the
+counterpositive of Proposition~\ref{thm:highes-weight-of-fin-dim-is-dominant}!
+If \(\lambda = k_1 \beta_1 + \cdots + k_r \beta_r \in P\) is integral and \(k_i
+< 0\) for all \(i\), then one is additionally able to show that \(M(\lambda)
+\cong L(\lambda)\) as in Example~\ref{ex:antidominant-verma}. Verma modules can
+thus serve as examples of infinite-dimensional simple modules.
+
+In the next chapter we expand our previous results by exploring the question:
+what are \emph{all} the infinite-dimensional simple \(\mathfrak{g}\)-modules?