Under Choice, every finitely generated nonzero module has a maximal proper submodule

Let $M\mathrm{\ne }0$ be generated over $R$ by $x_1,\dots ,x_n$ [L1] and let $\mathcal{P}$ be the set of proper submodules of $M$ [L2], ordered by inclusion. It is nonempty, since $0$ is a proper submodule of the nonzero module $M$.

Let $\mathcal{C}\subseteq \mathcal{P}$ be a chain. If $\mathcal{C}$ is empty, $0\in \mathcal{P}$ is an upper bound. Otherwise put $U=\bigcup \mathcal{C}$; any two elements of $U$ lie in a common member of the chain, so $U$ is a submodule. If $U=M$, each generator $x_i$ would lie in some member of $\mathcal{C}$, and the largest of those finitely many members would contain every $x_i$ and hence equal $M$, contradicting properness. So $U\in \mathcal{P}$ and is an upper bound for $\mathcal{C}$.

Every chain in the nonempty poset $\mathcal{P}$ therefore has an upper bound in $\mathcal{P}$, so Zorn's lemma [L3] — which assumes the Axiom of Choice, as the Statement does — gives a maximal element of $\mathcal{P}$, that is, a maximal proper submodule of $M$.

Both hypotheses are load-bearing above: nonzeroness is what makes the poset of step 1.1 nonempty, and finite generation is what makes the union of a chain proper in step 2.1. This proves the stated claim.