Zorn's Lemma in noetherian modules 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.
 A: I must say the argument seems fine to me.
Assuming no module in $S$ is maximal, we can construct a sequence $N_0\subsetneq N_1\subsetneq\ldots$ which contradicts the ACC condition.
But note you need the axiom of choice to construct the sequence, as it's not obvious at all how to choose the modules.
In fact, only the dependent choice is required.
A: This is a particularly delicate use of the axiom of choice. Historically the principle of dependent choice, which is used exactly for these sort of inductive constructions, was overlooked by some of the greatest people that opposed to the axiom (e.g. Lebesgue).
When we construct a sequence by induction, we can only assure that for every finite number $n$, we can construct a sequence of length $n$. The axiom of choice, or rather the much weaker principle of dependent choice, is needed to prove the existence of an infinite sequence from that.
Zorn's lemma is used in the following manner. Every chain is finite, therefore it has an upper bound. So there is a maximal element.
