[proofplan] To prove that the lexicographic order is a well-order, we take an arbitrary nonempty subset $S \subset A \times B$ and construct its least element. First we choose the least first coordinate appearing in $S$, using that $A$ is well-ordered. Then, among all elements of $S$ with that first coordinate, we choose the least second coordinate, using that $B$ is well-ordered. The resulting pair is shown directly to be below every element of $S$ in the lexicographic order. [/proofplan]

[step:Choose the least first coordinate appearing in the subset] Let $S \subset A \times B$ be nonempty. Define the projection set \begin{align*} P := \{a \in A : \text{there exists } b \in B \text{ such that } (a,b) \in S\}. \end{align*} Since $S$ is nonempty, there exists $(a_0,b_0) \in S$, so $a_0 \in P$. Hence $P$ is a nonempty subset of $A$. Because $(A,\leq_A)$ is well-ordered, $P$ has a least element. Denote this least element by $a_* \in P$. [/step]

[step:Choose the least second coordinate over the least first coordinate] Since $a_* \in P$, the fiber set \begin{align*} Q := \{b \in B : (a_*,b) \in S\} \end{align*} is nonempty. Because $(B,\leq_B)$ is well-ordered, $Q$ has a least element. Denote this least element by $b_* \in Q$. By the definition of $Q$, we have $(a_*,b_*) \in S$. [/step]

[step:Verify that the selected pair is least in the lexicographic order] Let $(a,b) \in S$ be arbitrary. Since $(a,b) \in S$, we have $a \in P$. Because $a_*$ is the least element of $P$, we have $a_* \leq_A a$. If $a_* <_A a$, then by the definition of $\leq_{\mathrm{lex}}$, \begin{align*} (a_*,b_*) \leq_{\mathrm{lex}} (a,b). \end{align*} If instead $a_* = a$, then $b \in Q$, because $(a_*,b) = (a,b) \in S$. Since $b_*$ is the least element of $Q$, we have $b_* \leq_B b$, and therefore, again by the definition of $\leq_{\mathrm{lex}}$, \begin{align*} (a_*,b_*) \leq_{\mathrm{lex}} (a,b). \end{align*} Thus $(a_*,b_*) \leq_{\mathrm{lex}} (a,b)$ for every $(a,b) \in S$. Since $(a_*,b_*) \in S$, it is the least element of $S$ under $\leq_{\mathrm{lex}}$. Therefore every nonempty subset of $A \times B$ has a least element, so $(A \times B,\leq_{\mathrm{lex}})$ is well-ordered. [/step]