Every finite partially ordered set, $(A, \leq)$, has a maximum length chain.
A chain is a sequence of distinct elements $a_1 \leq a_2 \leq .......\leq a_n$ with relation $"\leq"$ where $a_i \in A$ for all $i$
How to prove this formally using wellordering principle ? I see that if we need to prove there exist a minimal length chain it will be useful, but what is WOP's relation with proving maximal length chain ? Is it related to a bounded set has a max element ? if so how to use well ordering to show this ?