For noetherian modules, we have in particular the equivalent definitions that the Ascending Chain Condition holds and that every nonempty subset of submodules has a maximal element.
Now I can prove the "ACC $\Rightarrow$ every nonempty set of submodules has a maximal element" implication by the following argument:
Let $S$ be a nonempty set of submodules, take $N_1 \in S$. If $N_1$ is not maximal, there exists a $N_2 \supsetneq N_1$ per definition. By induction we get a chain $N_1 \subsetneq N_2 \subsetneq \dotsb$ and by ACC this induction terminates after finitely many, say $n$, steps. Then $N_n$ is maximal.
My question is: Did I miss the use of Zorn's Lemma somewhere? This proof doesn't seem to use it, and the other implications in the equivalence work fine without it too, yet I've seen some sources (e.g. Wikipedia, first answer here: Is every Noetherian module finitely generated?) that require it. I'm fine with Zorn's Lemma by the way, just feeling a bit stupid right now.