[proofplan] We cover the order complex $\triangle(\overline{L})$ by subcomplexes indexed by the crosscut elements. The crosscut condition ensures that every chain in the proper part lies in at least one member of the cover. We then identify the nerve of this cover by analyzing which intersections are nonempty and contractible; the meet or join of an indexing set supplies a cone point exactly when that indexing set is a face of the crosscut complex. The nerve lemma then gives the desired homotopy equivalence. [/proofplan] [step:Cover the order complex by comparability subcomplexes] For each $c\in C$, define $U_c$ to be the subcomplex of $\triangle(\overline{L})$ whose simplices are precisely the finite chains $x_0<x_1<\cdots<x_k$ in $\overline{L}$ such that every vertex $x_i$ is comparable with $c$ in $L$. We claim that the family $(U_c)_{c\in C}$ covers $\triangle(\overline{L})$. Let $\sigma$ be a simplex of $\triangle(\overline{L})$, so $\sigma$ is a finite chain in $\overline{L}$. Because $L$ is finite, $\sigma$ is contained in a maximal chain of $L$. Since $C$ is a crosscut, this maximal chain contains some element $c\in C$. Every two elements of a chain are comparable, so every vertex of $\sigma$ is comparable with this $c$. Hence $\sigma\in U_c$. Thus $\triangle(\overline{L})=\bigcup_{c\in C} U_c$. [/step] [step:Describe every finite intersection as an order complex] Let $A\subseteq C$. Define the subposet $P_A\subseteq \overline{L}$ by $P_A=\{x\in \overline{L}: x\text{ is comparable with every }c\in A\}$. For $A=\varnothing$, this definition gives $P_\varnothing=\overline{L}$. By the definition of the subcomplexes $U_c$, a simplex belongs to $\bigcap_{c\in A}U_c$ exactly when all of its vertices lie in $P_A$. Therefore $\bigcap_{c\in A}U_c=\triangle(P_A)$. [guided] We now translate an intersection of subcomplexes into an order complex of a single subposet. Fix a subset $A\subseteq C$. A simplex of $\triangle(\overline{L})$ is a chain in $\overline{L}$. It lies in $U_c$ precisely when every vertex of that chain is comparable with $c$. Therefore it lies in every $U_c$ with $c\in A$ precisely when every vertex is comparable with every element of $A$. This motivates the definition $P_A=\{x\in \overline{L}: x\text{ is comparable with every }c\in A\}$. The chains in $P_A$ are exactly the simplices in the intersection $\bigcap_{c\in A}U_c$. Hence the intersection is not merely homotopy equivalent to an order complex; it is equal to the order complex of this explicitly defined subposet: $\bigcap_{c\in A}U_c=\triangle(P_A)$. For the empty subset $A=\varnothing$, there is no comparability condition, so $P_\varnothing=\overline{L}$ and the corresponding intersection is the whole complex $\triangle(\overline{L})$. [/guided] [/step] [step:Use antichainness to force a common comparable element to be uniformly below or uniformly above] Let $A\subseteq C$ and let $x\in P_A$. If $|A|\ge 2$, then exactly one of the following two alternatives holds: \begin{align*} x\le c\text{ for every }c\in A \end{align*} or \begin{align*} c\le x\text{ for every }c\in A. \end{align*} Indeed, suppose there were $a,b\in A$ such that $x\le a$ and $b\le x$. Then $b\le a$. Since $C$ is an antichain and $a,b\in C$, this forces $a=b$. Thus no two distinct elements of $A$ can occur on opposite sides of $x$. Because $x$ is comparable with every element of $A$, all elements of $A$ must lie on the same side of $x$. For $|A|=1$, if $A=\{c\}$, then $P_A$ is the set of proper elements comparable with $c$, and the element $c$ itself will serve as both the meet and the join of $A$ in the cone arguments below. [/step] [step:Exhibit a cone point when the indexing set is a face of the crosscut complex] Assume first that $A\subseteq C$ satisfies \begin{align*} \bigwedge A>\hat{0}. \end{align*} Let \begin{align*} m=\bigwedge A. \end{align*} Since $m\le c$ for every $c\in A$ and each $c\in \overline{L}$, we have $m\ne\hat{1}$. Together with $m>\hat{0}$, this gives $m\in\overline{L}$. Also $m$ is comparable with every element of $A$, so $m\in P_A$. We show that $m$ is comparable with every element of $P_A$. Let $x\in P_A$. If $A=\varnothing$, then $m=\hat{1}$ is not in $\overline{L}$, so this case is excluded by the separate nerve convention for the empty intersection. If $|A|=1$, then $m$ is the unique element of $A$, and $x$ is comparable with $m$ by definition of $P_A$. If $|A|\ge 2$, the preceding step shows that either $x\le c$ for every $c\in A$ or $c\le x$ for every $c\in A$. In the first case, $x$ is a lower bound of $A$, so $x\le m$ by the greatest-lower-bound property of $m$. In the second case, $m\le c\le x$ for every $c\in A$. Thus $m$ is comparable with every $x\in P_A$. It follows that every simplex of $\triangle(P_A)$ can be enlarged by the vertex $m$, unless it already contains $m$. Hence $\triangle(P_A)$ is a cone with cone point $m$, and is contractible. The dual argument applies if \begin{align*} \bigvee A<\hat{1}. \end{align*} Let \begin{align*} j=\bigvee A. \end{align*} Then $j\in\overline{L}$, $j\in P_A$, and the same comparability argument, with upper and lower bounds interchanged, shows that $j$ is comparable with every element of $P_A$. Hence $\triangle(P_A)$ is a cone with cone point $j$, and is contractible. [/step] [step:Show that nonfaces give empty intersections] Let $A\subseteq C$ satisfy \begin{align*} \bigwedge A=\hat{0} \end{align*} and \begin{align*} \bigvee A=\hat{1}. \end{align*} We prove that $P_A=\varnothing$, and hence \begin{align*} \bigcap_{c\in A}U_c=\varnothing. \end{align*} The conditions exclude $A=\varnothing$ and $|A|=1$, because for $A=\varnothing$ the meet is $\hat{1}$ and the join is $\hat{0}$, while for $A=\{c\}$ both meet and join are $c\in\overline{L}$. Thus $|A|\ge 2$. Suppose, for contradiction, that $x\in P_A$. By the antichain argument above, either $x\le c$ for every $c\in A$ or $c\le x$ for every $c\in A$. In the first case, $x$ is a lower bound of $A$, so \begin{align*} x\le \bigwedge A=\hat{0}. \end{align*} This forces $x=\hat{0}$, contradicting $x\in\overline{L}$. In the second case, $x$ is an upper bound of $A$, so \begin{align*} \hat{1}=\bigvee A\le x. \end{align*} This forces $x=\hat{1}$, again contradicting $x\in\overline{L}$. Therefore $P_A=\varnothing$. [/step] [step:Identify the nerve with the crosscut complex] Let $\mathcal{N}$ denote the nerve of the cover $(U_c)_{c\in C}$. Its vertex set is $C$, and a subset $A\subseteq C$ is a face of $\mathcal{N}$ precisely when \begin{align*} \bigcap_{c\in A}U_c\ne\varnothing. \end{align*} For $A=\varnothing$, this condition holds by convention for nerves, and $\varnothing$ is also a face of $\Gamma(L,C)$. For nonempty $A\subseteq C$, the previous two steps show that $\bigcap_{c\in A}U_c$ is nonempty exactly when \begin{align*} \bigwedge A>\hat{0}\quad\text{or}\quad \bigvee A<\hat{1}. \end{align*} Indeed, if one of these inequalities holds, the intersection is a contractible cone and in particular is nonempty. If neither inequality holds, then $\bigwedge A=\hat{0}$ and $\bigvee A=\hat{1}$, and the intersection is empty. This is exactly the defining face condition for $\Gamma(L,C)$. Therefore \begin{align*} \mathcal{N}=\Gamma(L,C). \end{align*} [/step] [step:Apply the nerve lemma to obtain the homotopy equivalence] The cover $(U_c)_{c\in C}$ is a finite cover of the finite simplicial complex $\triangle(\overline{L})$ by subcomplexes. For every nonempty face $A$ of its nerve, the intersection $\bigcap_{c\in A}U_c$ is contractible by the cone-point argument above. Therefore the hypotheses of the nerve lemma are satisfied (citing a result not yet in the wiki: Nerve Lemma). The nerve lemma gives a homotopy equivalence between $\triangle(\overline{L})$ and the nerve of this cover. Since the nerve is $\Gamma(L,C)$, we obtain \begin{align*} \triangle(\overline{L})\simeq \Gamma(L,C). \end{align*} This is the desired homotopy equivalence. [/step]