ACC (DCC) implies upper (lower) sets are upper (lower) closure of antichains? I have read around (e.g. in Wikipedia) that if the ascending (descending) chain condition holds, all upper (lower) sets are the upper (lower) closure of an antichain, but I cannot find a proof. 
More precisely, let $(P, \leq)$ be a poset, $A(P)$ be the set of antichains on $P$, $U(P)$ be the set of upper sets on $P$ and $L(P)$ be the lower sets. Let $\uparrow$ ($\downarrow$) be the upper (lower) closure:
$$
  \uparrow S = \{p \in P: \exists s \in S: s\leq p  \}
$$
$$
  \downarrow S = \{p \in P: \exists s \in S: s \geq p\}
$$
Then I'm looking for a proof of the following:
Lemma (?): If DCC holds, then for all $u\in U(P)$, there exists $a\in A(P)$ such that $u=\,\uparrow a$.
Dually:
Lemma (?): If ACC holds, then for all $l\in L(P)$, there exists $a\in A(P)$ such that $l=\,\downarrow a$.
(I can see how this is true for finite posets but not more generally.)
 A: $\newcommand\P{\mathbb{P}}$Let $U$ be any upper set in a partial
order $\langle\P,\leq\rangle$, which satisfies the descending
chain condition, which asserts that every descending sequence of
points terminates. In other words, the order is a well-founded relation,
which is equivalent to saying that every nonempty subset of $\P$
has a minimal element. (Note that one needs the principle of dependent choice to prove that these characterizations are equivalent in all relations.) 
Let $A$ consist of the minimal elements of $U$. These form an
antichain (in the sense of pairwise incomparability). Since $A\subset U$ and $U$ is upward-closed, we clearly have 
$A{\uparrow}\subset U$. But the converse inclusion is also true, because if
$y\in U$, then consider the collection of $\{u\in U\mid u\leq
y\}$, which is a nonempty subset of $\P$. Thus, it has a minimal
element $a$, which is also minimal in $U$. So $a\in A$ and $a\leq
y$, which puts $y\in A{\uparrow}$. So $A{\uparrow}=U$, and thus $U$ is
the up-set of an antichain.
The dual situation for down-sets, using the ACC, is analogous.
Update. Finally, let me add that without the axiom of dependent choice, the lemmas are no longer necessarily true. For example, it is consistent with ZF that there is a tree of finite sequences, such that every sequence has an extension in the tree, but there is no infinite branch through the tree (basically, one is not able to choose successors successively in order to build the branch). If we orient this tree growing downwards, then the relation has the DCC, precisely because the tree has no infinite branch. But meanwhile, the whole tree is upward-closed, but it is not the up-set of an antichain, because every node in the tree has extensions below.
Since these kind of trees are intimately connected to the failure of dependent choice, this shows that the lemmas are actually each equivalent over ZF to the principle of dependent choice. 
