[proofplan] We order the facets of $\Delta(\overline{P})$ by the lexicographic order of the label words of the corresponding saturated chains from $\hat{0}$ to $\hat{1}$. For a fixed maximal chain, every descent in its label word can be repaired inside the corresponding rank-two interval by replacing the descending two-edge segment with the unique increasing segment supplied by the EL-labelling. This replacement produces an earlier facet differing in exactly one vertex. Finally, we choose the first block on which an earlier chain differs from the fixed chain, so the lexicographic comparison is forced inside that interval, and the shelling criterion follows from the resulting codimension-one deletion. [/proofplan]

[step:Translate facets into saturated chains from $\hat{0}$ to $\hat{1}$] Let $\Lambda$ be the totally ordered label set of the EL-labelling, and write \begin{align*} \lambda: \operatorname{Cov}(P) \to \Lambda \end{align*} for the labelling map, where $\operatorname{Cov}(P)$ denotes the set of cover relations $x \lessdot y$ in $P$. Since $P$ is finite, bounded, and graded, every maximal chain from $\hat{0}$ to $\hat{1}$ has the same length. Write this common length as $r \in \mathbb{N}$. A saturated maximal chain has the form \begin{align*} C: \hat{0} = x_0 \lessdot x_1 \lessdot \cdots \lessdot x_{r-1} \lessdot x_r = \hat{1}. \end{align*} It determines the facet \begin{align*} F_C := \{x_1, x_2, \dots, x_{r-1}\} \end{align*} of $\Delta(\overline{P})$, and every facet of $\Delta(\overline{P})$ arises uniquely in this way. Thus it is enough to shell the set of such facets. If $r \leq 1$, then $\overline{P} = \varnothing$, so the order complex has no non-empty facets and is shellable by the standard empty-complex convention. Hence assume $r \geq 2$. [/step]

[step:Order the facets by lexicographic label words] Let $\mathcal{C}$ denote the finite set of saturated maximal chains from $\hat{0}$ to $\hat{1}$. Define the label-word map \begin{align*} w:\mathcal{C}\to \Lambda^r \end{align*} as follows. For a saturated maximal chain \begin{align*} C: \hat{0} = x_0 \lessdot x_1 \lessdot \cdots \lessdot x_r = \hat{1}, \end{align*} define its label word by \begin{align*} w(C) := \bigl(\lambda(x_0, x_1), \lambda(x_1, x_2), \dots, \lambda(x_{r-1}, x_r)\bigr). \end{align*} Order the maximal chains first by the lexicographic order on their label words, and break ties by any fixed total order on the finite set of maximal chains. This gives a total ordering \begin{align*} C_1 \prec C_2 \prec \cdots \prec C_N \end{align*} of the saturated maximal chains from $\hat{0}$ to $\hat{1}$. We order the corresponding facets as \begin{align*} F_{C_1}, F_{C_2}, \dots, F_{C_N}. \end{align*} We will prove that this facet order is a shelling order. [/step]

[step:Replace each descent by an earlier chain differing in one vertex]Fix a saturated maximal chain \begin{align*} C: \hat{0} = x_0 \lessdot x_1 \lessdot \cdots \lessdot x_r = \hat{1}. \end{align*} For $1 \leq i \leq r-1$, call $i$ a descent position of $C$ if \begin{align*} \lambda(x_{i-1}, x_i) > \lambda(x_i, x_{i+1}). \end{align*} Assume $i$ is a descent position. Consider the interval $[x_{i-1}, x_{i+1}]$. Since $P$ is graded and $x_{i-1} \lessdot x_i \lessdot x_{i+1}$, this interval has rank two. The EL-property applied to $[x_{i-1}, x_{i+1}]$ gives a unique saturated chain \begin{align*} x_{i-1} \lessdot y_i \lessdot x_{i+1} \end{align*} whose two-edge label word is weakly increasing, and this word is lexicographically smallest among all saturated chains in the interval. Because the original two-edge segment through $x_i$ has a descent, it is not weakly increasing. Therefore $y_i \neq x_i$, and the label word of \begin{align*} x_{i-1} \lessdot y_i \lessdot x_{i+1} \end{align*} is lexicographically smaller than the label word of \begin{align*} x_{i-1} \lessdot x_i \lessdot x_{i+1}. \end{align*} Define the saturated maximal chain $D_i$ by replacing $x_i$ with $y_i$ and leaving every other vertex unchanged: \begin{align*} D_i: \hat{0} = x_0 \lessdot x_1 \lessdot \cdots \lessdot x_{i-1} \lessdot y_i \lessdot x_{i+1} \lessdot \cdots \lessdot x_r = \hat{1}. \end{align*} The label words of $D_i$ and $C$ agree before position $i$, and at the interval beginning at $x_{i-1}$ the word of $D_i$ is lexicographically smaller. Hence $D_i \prec C$. Moreover $F_C \setminus F_{D_i} = \{x_i\}$.[/step]

[guided]The purpose of this step is to show that a descent in the label word produces exactly the codimension-one predecessor needed for shellability. Fix a descent position $i$, so \begin{align*} \lambda(x_{i-1}, x_i) > \lambda(x_i, x_{i+1}). \end{align*} We focus only on the rank-two interval $[x_{i-1}, x_{i+1}]$. The chain segment through $x_i$ is saturated in this interval: \begin{align*} x_{i-1} \lessdot x_i \lessdot x_{i+1}. \end{align*} The EL-labelling condition says that every interval has a unique weakly increasing saturated chain, and that this chain is lexicographically first among all saturated chains in that interval. Applying this to $[x_{i-1}, x_{i+1}]$, there exists a unique element $y_i \in [x_{i-1}, x_{i+1}]$ such that \begin{align*} x_{i-1} \lessdot y_i \lessdot x_{i+1} \end{align*} has weakly increasing label word and is lexicographically minimal in the interval. The original segment through $x_i$ is not weakly increasing, because its first label is strictly larger than its second label. Therefore it cannot be the EL-increasing segment. Thus $y_i \neq x_i$. Since the increasing segment is lexicographically first in the interval, its two-label word is lexicographically smaller than the two-label word of the segment through $x_i$. Now replace only the vertex $x_i$ by $y_i$ and keep all other vertices of $C$ fixed. This gives \begin{align*} D_i: \hat{0} = x_0 \lessdot x_1 \lessdot \cdots \lessdot x_{i-1} \lessdot y_i \lessdot x_{i+1} \lessdot \cdots \lessdot x_r = \hat{1}. \end{align*} The new chain is saturated because the replacement segment is saturated in the same rank-two interval. Its label word agrees with $w(C)$ up to the edge entering $x_{i-1}$, and then becomes lexicographically smaller on the two-edge segment from $x_{i-1}$ to $x_{i+1}$. Therefore $D_i \prec C$. Finally, the two facets differ in exactly one vertex. The facet $F_C$ contains $x_i$, while $F_{D_i}$ contains $y_i$ instead, and all other internal vertices are the same. Hence $F_C \setminus F_{D_i} = \{x_i\}$.[/guided]

[step:Find a missing descent vertex against every earlier chain] Let $D \prec C$ be an earlier saturated maximal chain, where \begin{align*} D: \hat{0} = z_0 \lessdot z_1 \lessdot \cdots \lessdot z_r = \hat{1}. \end{align*} Since $D \neq C$, there is at least one rank $j$ with $z_j \neq x_j$. Choose $a < b$ so that $a+1$ is the first rank at which the two chains differ, $x_a = z_a$, $x_b = z_b$, and $x_j \neq z_j$ for every $a < j < b$. Equivalently, $a < j < b$ is the first maximal block of consecutive internal ranks on which the two chains differ. The endpoints exist because $x_0 = z_0 = \hat{0}$ and $x_r = z_r = \hat{1}$. We claim that the segment \begin{align*} x_a \lessdot x_{a+1} \lessdot \cdots \lessdot x_b \end{align*} has a descent. Suppose not. Then its label word is weakly increasing. By the EL-property in the interval $[x_a, x_b]$, this weakly increasing saturated chain is the unique increasing chain and is lexicographically first in that interval. If the corresponding segment $z_a \lessdot z_{a+1} \lessdot \cdots \lessdot z_b$ had lexicographically smaller label word, then the segment of $C$ would not be lexicographically first in $[x_a, x_b]$, a contradiction. If the two segment label words were equal, then the segment through the $z_j$ would also be weakly increasing. Since the endpoints agree and the two chains differ at every internal rank between $a$ and $b$, this would give a second weakly increasing saturated chain in $[x_a, x_b]$, contradicting uniqueness in the EL-property. Because this is the first block on which $C$ and $D$ differ, the global lexicographic comparison between $w(D)$ and $w(C)$ is determined by the two segment label words in $[x_a, x_b]$. Thus $D$ cannot precede $C$, contradicting $D \prec C$. Therefore there exists an index $i$ with $a < i < b$ such that \begin{align*} \lambda(x_{i-1}, x_i) > \lambda(x_i, x_{i+1}). \end{align*} By construction of the first disagreement block, $x_i \neq z_i$, and since both chains are graded, a vertex of rank $i$ in $F_C$ can equal a vertex of $F_D$ only if it is $z_i$. Hence $x_i \notin F_D$. [/step]

[step:Verify the shelling condition] We use the following facet criterion for shellability: a total order $F_{C_1}, \dots, F_{C_N}$ of the facets of a pure simplicial complex is a shelling order if, for every $C_j$ and every earlier $C_k \prec C_j$, there exists an earlier chain $C_\ell \prec C_j$ and a vertex $v \in F_{C_j} \setminus F_{C_k}$ such that $F_{C_j} \setminus F_{C_\ell} = \{v\}$. Fix $C$ and an earlier chain $D \prec C$. By the previous step, there is a descent position $i$ of $C$ such that $x_i \notin F_D$. By the descent-replacement step, the chain $D_i$ satisfies $D_i \prec C$ and $F_C \setminus F_{D_i} = \{x_i\}$. Since $x_i \notin F_D$, this is exactly the codimension-one deletion required by the shelling criterion for the pair $F_D, F_C$. Because $D \prec C$ was arbitrary, the lexicographic facet order satisfies the shelling condition at every facet. Thus the order \begin{align*} F_{C_1}, F_{C_2}, \dots, F_{C_N} \end{align*} is a shelling order of $\Delta(\overline{P})$. Hence $\Delta(\overline{P})$ is shellable. [/step]