The sum of solvable ideals is solvable

The subspace $\mathfrak{i}+\mathfrak{j}$ is an ideal because both summands are ideals. The map $\mathfrak{j}\to (\mathfrak{i}+\mathfrak{j})\mathrm{/}\mathfrak{i}$, $y\mapsto y+\mathfrak{i}$, is a surjective Lie homomorphism with kernel $\mathfrak{i}\cap \mathfrak{j}$, so it induces the explicit isomorphism $\mathfrak{j}\mathrm{/}(\mathfrak{i}\cap \mathfrak{j})\cong (\mathfrak{i}+\mathfrak{j})\mathrm{/}\mathfrak{i}$.

If $\mathfrak{i}$ and $\mathfrak{j}$ are solvable, [L2] makes the quotient in step 1.1 solvable; applying [L2] again to the ideal $\mathfrak{i}$ in $\mathfrak{i}+\mathfrak{j}$ proves that the sum is solvable. Repetition gives the same result for every specified finite sum, including the empty sum $0$.

Let $R$ be the algebraic sum of all solvable ideals of finite-dimensional $\mathfrak{g}$. It is an ideal and contains each such ideal. Choose a finite basis $r_1,\dots ,r_t$ of $R$; by the definition of algebraic sum, each $r_s$ belongs to a finite sum of solvable ideals. Collecting the finitely many ideals occurring in these finitely many expressions gives solvable ideals $I_1,\dots ,I_N$ with $R=I_1+\cdots +I_N$. Step 2.1 makes $R$ solvable, so [L1] identifies it as $\mathrm{rad}(\mathfrak{g})$; any two largest ideals contain one another and are equal. All selections are finite after one finite basis is fixed, so AC is not used.