If $M$ is a Noetherian $R$-module, every non-empty set of proper submodules of $M$ has a maximal element 
Let $M$ be a Noetherian $R$-module. Show that every non-empty set of proper submodules of $M$ has a maximal element.

My proof:
Suppose for a contradiction that we have set of proper submodules of $M$, let's call it $\mathfrak{M}$, which is non-empty and does not have a maximal element. Choose $N_1 \in \mathfrak{M}$, then it can't be maximal so there's $N_2 \in \mathfrak{M}$ with $N_1 \subsetneq N_2$. But $N_2$ is not maximal, so $\ \exists \ N_3 \in \mathfrak{M}$ such that $N_2 \subsetneq N_3$. Thus we can construct a chain $N_1 \subsetneq N_2 \subsetneq N_3 \subsetneq \dots$, but $M$ is Noetherian, hence this is a contradiction. Thus $\mathfrak{M}$ has a maximal element with respect to inclusion.
Is my proof correct? I'm having some doubts because I recall needing Zorn's lemma to prove this kind of statements.
 A: Two comments.
First, there is no need to formulate the proof by contradiction; you simply show the contrapositive! That is, if there is some non-empty collection of submodules without a maximal element then there is some non-stabilizing properly ascending chain of submodules. This is just a general note on style. The proof is correct, though (the part rschwieb mentioned in the comments is important but essentially taking care of by requiring $\mathfrak M$ to not have maximal elements; and $M$ is maximal...).
Second, you do not need Zorn's Lemma (i.e. the full Axiom of Choice) but some related, strictly weaker choice principle called the axiom of dependent choice. However, to the best of my knowledge there is no way of avoiding the usage of any choice principle at all in showing this implication. So it matters which definition of Noetherian you are using when you are simultaneously interested in these kinds of things.
This is by the way an interesting elementary application of a choice principle within algebra which is not "every vector space has a basis" or "every field has an algebraic closure".
