[proofplan] We order the solvable ideals of $\mathfrak g$ by dimension and choose one of maximal dimension, using finite-dimensionality. The key algebraic point is that the sum of two solvable ideals is again a solvable ideal; we prove this directly from the derived series. Once this closure property is established, maximality forces the chosen solvable ideal to contain every other solvable ideal, and uniqueness follows from mutual containment. [/proofplan]

[step:Choose a solvable ideal of maximal dimension] Let $k$ denote the base field of $\mathfrak g$. Let $\mathbb N := \{1,2,3,\dots\}$ denote the set of positive integers. For every finite-dimensional $k$-[vector space](/page/Vector%20Space) $V$, let $\dim_k V$ denote the dimension of $V$ over $k$. For a Lie subalgebra $\mathfrak b \subseteq \mathfrak g$, the notation $\mathfrak b \trianglelefteq \mathfrak g$ means that $\mathfrak b$ is an ideal of $\mathfrak g$, namely $[x,y] \in \mathfrak b$ for all $x \in \mathfrak g$ and $y \in \mathfrak b$. For any Lie algebra $\mathfrak h$, define its derived series by \begin{align*} \mathfrak h^{(0)} &:= \mathfrak h, & \mathfrak h^{(m+1)} &:= [\mathfrak h^{(m)}, \mathfrak h^{(m)}] \quad \text{for } m \geq 0. \end{align*} The Lie algebra $\mathfrak h$ is solvable if there exists $m \in \mathbb N$ such that $\mathfrak h^{(m)} = 0$. Let $\mathcal S$ denote the set of all solvable ideals of $\mathfrak g$: \begin{align*} \mathcal S := \{\mathfrak a \trianglelefteq \mathfrak g : \mathfrak a \text{ is solvable}\}. \end{align*} The zero ideal $0 \trianglelefteq \mathfrak g$ belongs to $\mathcal S$, so $\mathcal S$ is nonempty. Since $\mathfrak g$ is finite-dimensional over $k$, every ideal of $\mathfrak g$ has dimension in the finite set $\{0,1,\dots,\dim_k \mathfrak g\}$. Hence there exists $\mathfrak r \in \mathcal S$ such that \begin{align*} \dim_k \mathfrak r = \max\{\dim_k \mathfrak a : \mathfrak a \in \mathcal S\}. \end{align*} [/step]

[step:Show that the sum of two solvable ideals is solvable] Let $\mathfrak r \trianglelefteq \mathfrak g$ and $\mathfrak a \trianglelefteq \mathfrak g$ be solvable ideals. We prove that $\mathfrak r+\mathfrak a$ is a solvable ideal of $\mathfrak g$. First, $\mathfrak r+\mathfrak a$ is an ideal: for $x \in \mathfrak g$, $u \in \mathfrak r$, and $v \in \mathfrak a$, \begin{align*} [x,u+v] = [x,u] + [x,v] \in \mathfrak r+\mathfrak a, \end{align*} because $\mathfrak r$ and $\mathfrak a$ are ideals. We next prove solvability. Since $\mathfrak r$ is an ideal of $\mathfrak g$, each derived term $\mathfrak r^{(j)}$ is also an ideal of $\mathfrak g$. Indeed, if $\mathfrak b \trianglelefteq \mathfrak g$ is an ideal, then for $x \in \mathfrak g$ and $[y,z] \in [\mathfrak b,\mathfrak b]$, the Jacobi identity gives \begin{align*} [x,[y,z]] = [[x,y],z] + [y,[x,z]] \in [\mathfrak b,\mathfrak b], \end{align*} because $[x,y],[x,z] \in \mathfrak b$. We claim that for every $j \geq 0$, \begin{align*} (\mathfrak r+\mathfrak a)^{(j)} \subseteq \mathfrak r^{(j)}+\mathfrak a. \end{align*} For $j=0$, this is equality. Suppose it holds for some $j \geq 0$. Then \begin{align*} (\mathfrak r+\mathfrak a)^{(j+1)} &= [(\mathfrak r+\mathfrak a)^{(j)},(\mathfrak r+\mathfrak a)^{(j)}] \\ &\subseteq [\mathfrak r^{(j)}+\mathfrak a,\mathfrak r^{(j)}+\mathfrak a] \\ &\subseteq [\mathfrak r^{(j)},\mathfrak r^{(j)}]+[\mathfrak r^{(j)},\mathfrak a]+[\mathfrak a,\mathfrak r^{(j)}]+[\mathfrak a,\mathfrak a]. \end{align*} Since $\mathfrak r^{(j)} \trianglelefteq \mathfrak g$ and $\mathfrak a \trianglelefteq \mathfrak g$, we have \begin{align*} [\mathfrak r^{(j)},\mathfrak a] \subseteq \mathfrak r^{(j)} \cap \mathfrak a, \qquad [\mathfrak a,\mathfrak r^{(j)}] \subseteq \mathfrak r^{(j)} \cap \mathfrak a, \qquad [\mathfrak a,\mathfrak a] \subseteq \mathfrak a. \end{align*} Therefore \begin{align*} (\mathfrak r+\mathfrak a)^{(j+1)} \subseteq \mathfrak r^{(j+1)}+\mathfrak a. \end{align*} This proves the claim by induction. Because $\mathfrak r$ is solvable, choose $m \in \mathbb N$ such that $\mathfrak r^{(m)}=0$. The claim gives \begin{align*} (\mathfrak r+\mathfrak a)^{(m)} \subseteq \mathfrak a. \end{align*} Because $\mathfrak a$ is solvable, choose $n \in \mathbb N$ such that $\mathfrak a^{(n)}=0$. Since taking commutators preserves inclusion of Lie subalgebras, the inclusion $(\mathfrak r+\mathfrak a)^{(m)} \subseteq \mathfrak a$ implies \begin{align*} (\mathfrak r+\mathfrak a)^{(m+n)} \subseteq \mathfrak a^{(n)} = 0. \end{align*} Thus $\mathfrak r+\mathfrak a$ is solvable. [/step]

[step:Use maximality to prove that the chosen ideal contains every solvable ideal] Let $\mathfrak a \trianglelefteq \mathfrak g$ be any solvable ideal. By the previous step, $\mathfrak r+\mathfrak a$ is a solvable ideal of $\mathfrak g$, so $\mathfrak r+\mathfrak a \in \mathcal S$. Since $\mathfrak r \subseteq \mathfrak r+\mathfrak a$, maximality of $\dim_k \mathfrak r$ gives \begin{align*} \dim_k(\mathfrak r+\mathfrak a) = \dim_k \mathfrak r. \end{align*} The inclusion $\mathfrak r \subseteq \mathfrak r+\mathfrak a$ between finite-dimensional vector spaces of equal dimension is equality. Hence \begin{align*} \mathfrak r+\mathfrak a = \mathfrak r, \end{align*} and therefore $\mathfrak a \subseteq \mathfrak r$. [/step]

[step:Identify the radical and prove uniqueness] The ideal $\mathfrak r$ is solvable by construction and contains every solvable ideal of $\mathfrak g$ by the previous step. Define \begin{align*} \operatorname{rad}(\mathfrak g) := \mathfrak r. \end{align*} Then $\operatorname{rad}(\mathfrak g)$ is a largest solvable ideal of $\mathfrak g$. It remains to prove uniqueness. Suppose $\mathfrak r_1 \trianglelefteq \mathfrak g$ and $\mathfrak r_2 \trianglelefteq \mathfrak g$ are both largest solvable ideals of $\mathfrak g$, meaning that each is solvable and each contains every solvable ideal of $\mathfrak g$. Since $\mathfrak r_1$ is a solvable ideal, the largeness of $\mathfrak r_2$ gives $\mathfrak r_1 \subseteq \mathfrak r_2$. Since $\mathfrak r_2$ is a solvable ideal, the largeness of $\mathfrak r_1$ gives $\mathfrak r_2 \subseteq \mathfrak r_1$. Therefore \begin{align*} \mathfrak r_1 = \mathfrak r_2. \end{align*} Thus $\operatorname{rad}(\mathfrak g)$ exists and is unique. [/step]