Every finite group has a composition series

If $\mathrm{\mid }G\mathrm{\mid }=1$, the one-term chain $G=1$ is a composition series of length zero.

Assume $\mathrm{\mid }G\mathrm{\mid }>1$ and that every group of order smaller than $\mathrm{\mid }G\mathrm{\mid }$ has a composition series.

The finite nonempty set of proper normal subgroups of $G$ contains $1$, so choose one, say $N$, of maximum cardinality. This is finite maximization and uses no choice principle.

The quotient $G\mathrm{/}N$ is simple: a nontrivial proper normal subgroup of $G\mathrm{/}N$ would correspond by [L1] to a proper normal subgroup of $G$ strictly containing $N$, contrary to maximality.

Since $N$ is proper, $\mathrm{\mid }N\mathrm{\mid }<\mathrm{\mid }G\mathrm{\mid }$, so the induction hypothesis supplies a composition series $N=N_0▹\cdots ▹N_r=1$.

Prepending $G▹N$ to the series of step 3.2 gives a strict subnormal series whose new factor $G\mathrm{/}N$ is simple by step 3.1 and whose remaining factors are simple by induction; hence it is a composition series of $G$.