Is this proof legal? Let $\left(P,\le\right)$ denote a poset. 
Statement: if every sequence
$p_{1}\leq p_{2}\leq\cdots$ in $P$ stabilizes (in the sense that for some $n$ we have $k>n\Rightarrow p_k=p_n$) then every non-empty
subset of $P$ contains a maximal element.
Own effort: 
Let $S$ be a non-empty subset of $P$ that contains no
maximal element. Choose some $p_{1}\in S$. 
Then $p_{1}$ is not maximal
so some $p_{2}\in S$ exists with $p_{1}<p_{2}$. Repeating this we
come to a non-stabilizing sequence $p_{1}<p_{2}<\cdots$ in $S$.
However, I do not feel comfortable about this proof. I am 'choosing'
elements here, so should there not be some appeal on the axiom of
choice? Is it not just a proof by induction that for any $n$ there
we can find $p_{1},\cdots,p_{n}\in S$ such that $p_{1}<\cdots<p_{n}$?
Is the statement correct?
Underlying was the thought: can the A.C.C. condition for Noetherian modules be replaced by the statement that any non-empty subset of submodules has a maximal element?
 A: Here is an example when this doesn't work.
Suppose that $A_i$ for $i\in\Bbb N$ is a non-empty set, and there is choice function on them, meaning $\prod_{i\in\Bbb N}A_i$ is non-empty. 
Now consider the partial order $P=\bigcup_{n\in\Bbb N}\prod_{i<n}A_i$, ordered by inclusion. Meaning we choose from finitely many subsets, and going up meaning we choose from more elements.
If we had an infinite [strictly increasing] sequence, then its union would necessarily be a choice function from the entire family. So every sequence is necessarily finite (= stabilizes). But there is no maximal element.

So you need the axiom of choice, to some extent. How much do we need? Certainly countable choice, but in fact a little bit more.

The Principle of Dependent Choice. If $(P,\leq)$ is a partial order such that every finite chain can be extended, then there is a countably infinite chain.

In other words, if every finite chain stabilizes, then at least one of the chains reaches a maximal element. And this is exactly what you want here. This principle is stronger than just countable choice, but it is still much weaker than the axiom of choice itself.
A: I think here, to say "Repeating this we come to a non-stabilizing sequence $p_1 < p_2 < \dots$ in $S$" you need the axiom of dependent choice. In the hypothesis, you really need the whole sequence, not finite subsequences. This axiom implies the axiom of countable choice, which isn't a consequence of ZF.
A: You avoid the axiom of choice here, since you at any step in your proof have only done a finite number of choices. The axiom of choice is a whole lot stronger than that (it allows you to do all choices simultaneously, no matter how many choices you have to make, while you're making choices one by one), and hence not necessary. Your work is a fine proof by contradiction.
