Theorem: Dilworth's Theorem

Let $\struct {S, \preccurlyeq}$ be a finite ordered set.
Then the maximal size of an antichain is equal to the minimal number of pairwise disjoint chains in $\struct {S, \preccurlyeq}$ that partition $S$.
That is:
:$\min \set {k : \exists C_1, \dots C_k \subseteq S \text { chains such that } C_1 \mathop {\dot \cup} \dots \mathop {\dot \cup} C_k = S} = \max \set {\card A: A \subseteq S \text { is an antichain} }$
where $\dot \cup$ denotes disjoint union.

Proof:
Let $m$ denote the minimal number of chains needed to partition $S$.
Let $M$ denote the maximal size of an antichain in $S$.
Moreover let $A$ be an antichain of size $M$.
Let $C_1, C_2 \dots C_m$ be chains that partition $S$.
By definition of partition:
:$C_1, C_2 \dots C_m$ are pairwise disjoint
:$C_1, C_2 \dots C_m$ form a cover of $S$.
By the definition of antichain, no two elements of $A$ can lie in the same chain $C_i, i = 1 \dots m$.
This shows $M \le m$.
{{qed|lemma}}
For the converse inequality we proceed by induction on the cardinality $\card S$ of $S$. 
The base case for $\card S = 1$ is trivially true.
Suppose $\card S = n$ and that all ordered sets \(S'\) of cardinality $<n$ can be partitioned into \(M'\) chains $C_1, \dots C_{M'}$, where \(M'\) is  the maximal size of an antichain in \(S'\).
Let $C \subseteq S$ be a chain of maximal size.
We distinguish two cases:
;First Case:
:$S \setminus C$ does not contain an antichain of size $M$. 
Then, by the induction hypothesis, $S \setminus C$ can be covered by (at most) $M - 1$ disjoint chains.
Adding $C$ to this collection of chains yields a covering of $S$ by (at most) $M$ disjoint chains.
;Second Case:
There is an antichain of size $M$ in $S \setminus C$. 
Let $A = \set {a_1, \dots a_M}$ denote this antichain.
We define:
:$S^+ := \set {s \in S : \exists i \in \set {1, \ldots M}: s \succcurlyeq a_i}$
and:
:$S^- := \set {s \in S : \exists i \in \set {1, \ldots M}: s \preccurlyeq a_i}$
First we argue that $S^+ \cap S^- = A$: 
By  reflexivity of the ordering we have $A \subseteq S^+, A \subseteq S^-$.
For the other inclusion let $s \in S^+ \cap S^-$.
Then there are $i, j \in \set {1, \dots M}$ such that $s \preccurlyeq a_i$ and $a_j \preccurlyeq s$.
Since $a_i, a_j$ are elements of the antichain $A$ this implies $i = j$.
Otherwise $a_j \preccurlyeq a_i$ by transitivity).
Therefore $s = a_j = a_i \in A$ by antisymmetry.
That is:
:$A= S^+ \cap S^-$
Next we show $S^+ \cup S^- = S$:
The inclusion $S^+ \cup S^- \subseteq S$ is trivially fulfilled.
Next the other inclusion.
{{AimForCont}} there is an $s \in S \setminus \paren {S^+ \cup S^-}$.
Then $s \notin A$ and $\lnot \paren {a_i \preccurlyeq s}, \lnot \paren {s \preccurlyeq a_i}$ for all $i = 1 \dots M$.
Therefore $A \cup \set s$ is an antichain of size $M + 1$, in contradiction of the maximality of $A$.
Therefore:
:$S = S^+ \cup S^-$
Finally we argue that $\card {S^+} < \card S$ and $\card {S^-} < \card S$:
{{AimForCont}} $\card S = \card {S^+}$.
Then we have $S = S^+$.
Let $x:= \min C$.
Then $x \in S^+$
So there exists an $i \in \set {1 \dots M}$ such that $a_i \preccurlyeq x$.
By our assumption we have $a_i \notin C$.
Therefore $C \cup \set x \supsetneq C$ is a chain that strictly contains $C$.
This contradicts the maximality of $C$.
Therefore we must have $\card {S^+} < \card S$.
A symmetric argument shows that $\card {S^-} < \card S$.
We now can apply the induction hypothesis to $S^+, S^-$.
We obtain disjoint chains $D_i, E_i$ where $i \in \set {1, \dots M}$ such that:
:$S^+ = D_1 \dot\cup \dots \dot\cup D_m$
and:
:$S^- = E_1 \dot\cup \dots \dot\cup E_m$
Up to a potential renumbering and considering the definitions of $S^+$ and $S^-$, we may assume that $a_i = \min D_i = \max E_i$ for all $i \in \set {1, \dots M}$.
Therefore $C_i := D_i \cup E_i$ is a disjoint covering of $S$ by $M$ chains.
{{qed}}