[proofplan] We prove each assertion directly from the definitions. First, a subset of a face in the link or closed star still satisfies the same defining containment condition because $K$ is closed under taking subsets. Next, every face in the closed star splits into the part lying in $\sigma$ and the part disjoint from $\sigma$, and the latter part is exactly a face of the link. Finally, the link-of-a-link identity follows by expanding the two link definitions and comparing the resulting disjointness and membership conditions. [/proofplan] [step:Verify that the link is closed under taking faces] Let $L := \operatorname{lk}_K(\sigma)$. Every element of $L$ is a finite subset of $V$ because $L \subset K$ and $K$ is a simplicial complex on $V$. Since $\sigma \in K$, the empty face satisfies $\varnothing \cap \sigma = \varnothing$ and $\varnothing \cup \sigma = \sigma \in K$, so $\varnothing \in L$. Let $\eta \in L$, and let $\eta_0 \subset \eta$ be a subset. Since $\eta \in K$ and $K$ is closed under subsets, $\eta_0 \in K$. Since $\eta \cap \sigma = \varnothing$, we also have $\eta_0 \cap \sigma = \varnothing$. Finally, \begin{align*} \eta_0 \cup \sigma \subset \eta \cup \sigma. \end{align*} Because $\eta \cup \sigma \in K$ and $K$ is closed under subsets, $\eta_0 \cup \sigma \in K$. Therefore $\eta_0 \in L$. Thus $\operatorname{lk}_K(\sigma)$ is a simplicial complex. [/step] [step:Verify that the closed star is closed under taking faces] Let $S := \operatorname{st}_K(\sigma)$. Every element of $S$ is a finite subset of $V$ because $S \subset K$. Since $\sigma \in K$, the empty face satisfies $\varnothing \cup \sigma = \sigma \in K$, so $\varnothing \in S$. Let $\alpha \in S$, and let $\alpha_0 \subset \alpha$ be a subset. Since $\alpha \in K$ and $K$ is closed under subsets, $\alpha_0 \in K$. Also, \begin{align*} \alpha_0 \cup \sigma \subset \alpha \cup \sigma. \end{align*} Because $\alpha \cup \sigma \in K$ and $K$ is closed under subsets, $\alpha_0 \cup \sigma \in K$. Hence $\alpha_0 \in S$. Thus $\operatorname{st}_K(\sigma)$ is a simplicial complex. [/step] [step:Decompose each face of the closed star into its part inside $\sigma$ and its linked part] We prove both inclusions. First let $\alpha \in \operatorname{st}_K(\sigma)$. Define \begin{align*} \rho := \alpha \cap \sigma \end{align*} and \begin{align*} \eta := \alpha \setminus \sigma. \end{align*} Then $\rho \subset \sigma$, and $\alpha = \rho \cup \eta$. Since $\eta \subset \alpha$ and $\alpha \in K$, closure of $K$ under subsets gives $\eta \in K$. Also $\eta \cap \sigma = \varnothing$ by definition of set difference. Since $\alpha \in \operatorname{st}_K(\sigma)$, we have $\alpha \cup \sigma \in K$. Therefore \begin{align*} \eta \cup \sigma \subset \alpha \cup \sigma, \end{align*} so $\eta \cup \sigma \in K$. Hence $\eta \in \operatorname{lk}_K(\sigma)$, and $\alpha$ belongs to the right-hand side. Conversely, let $\rho \subset \sigma$ and let $\eta \in \operatorname{lk}_K(\sigma)$. Define \begin{align*} \alpha := \rho \cup \eta. \end{align*} Because $\eta \in \operatorname{lk}_K(\sigma)$, we have $\eta \cup \sigma \in K$. Since \begin{align*} \alpha = \rho \cup \eta \subset \sigma \cup \eta, \end{align*} closure under subsets gives $\alpha \in K$. Moreover, \begin{align*} \alpha \cup \sigma = \rho \cup \eta \cup \sigma = \eta \cup \sigma \in K. \end{align*} Therefore $\alpha \in \operatorname{st}_K(\sigma)$. This proves \begin{align*} \operatorname{st}_K(\sigma)=\{\rho \cup \eta : \rho \subset \sigma,\ \eta \in \operatorname{lk}_K(\sigma)\}. \end{align*} [guided] We want to show that the closed star consists exactly of faces obtained by choosing some part of $\sigma$ and then adding a face from the link. The natural way to find those two pieces is to take a face $\alpha$ in the closed star and split it according to whether its vertices lie in $\sigma$. Let $\alpha \in \operatorname{st}_K(\sigma)$. Define the two finite subsets of $V$ \begin{align*} \rho := \alpha \cap \sigma \end{align*} and \begin{align*} \eta := \alpha \setminus \sigma. \end{align*} Then $\rho \subset \sigma$, and the two pieces reconstruct $\alpha$: \begin{align*} \alpha = \rho \cup \eta. \end{align*} The point is now to prove that $\eta$ is not merely disjoint from $\sigma$, but is actually in the link of $\sigma$. Since $\eta \subset \alpha$ and $\alpha \in K$, the simplicial-complex axiom gives $\eta \in K$. By construction, $\eta \cap \sigma = \varnothing$. Finally, because $\alpha \in \operatorname{st}_K(\sigma)$, the definition of the closed star gives $\alpha \cup \sigma \in K$. Since \begin{align*} \eta \cup \sigma \subset \alpha \cup \sigma, \end{align*} the same closure-under-subsets axiom gives $\eta \cup \sigma \in K$. These are exactly the defining conditions for $\eta \in \operatorname{lk}_K(\sigma)$. Thus every $\alpha \in \operatorname{st}_K(\sigma)$ belongs to the set \begin{align*} \{\rho \cup \eta : \rho \subset \sigma,\ \eta \in \operatorname{lk}_K(\sigma)\}. \end{align*} For the reverse inclusion, start with a subset $\rho \subset \sigma$ and a face $\eta \in \operatorname{lk}_K(\sigma)$. Define \begin{align*} \alpha := \rho \cup \eta. \end{align*} Because $\eta$ is in the link, $\eta \cup \sigma \in K$. Since $\rho \subset \sigma$, we have \begin{align*} \alpha = \rho \cup \eta \subset \sigma \cup \eta. \end{align*} Therefore $\alpha \in K$ by closure under subsets. To prove that $\alpha$ lies in the closed star, we must also check that $\alpha \cup \sigma \in K$. But \begin{align*} \alpha \cup \sigma = \rho \cup \eta \cup \sigma = \eta \cup \sigma, \end{align*} and the final set belongs to $K$ because $\eta \in \operatorname{lk}_K(\sigma)$. Hence $\alpha \in \operatorname{st}_K(\sigma)$. The two inclusions prove the desired decomposition. [/guided] [/step] [step:Expand the definitions to identify the link of a link] Assume $\tau \in \operatorname{lk}_K(\sigma)$, and set $L := \operatorname{lk}_K(\sigma)$. Since $\tau \in L$, the expression $\operatorname{lk}_L(\tau)$ is defined. Also $\tau \cap \sigma = \varnothing$ and $\sigma \cup \tau \in K$, so $\sigma \cup \tau$ is a face of $K$. Let $\eta$ be a finite subset of $V$. By definition of link inside the simplicial complex $L$, \begin{align*} \eta \in \operatorname{lk}_L(\tau) \iff \eta \in L,\ \eta \cap \tau = \varnothing,\ \eta \cup \tau \in L. \end{align*} Expanding the two conditions involving $L=\operatorname{lk}_K(\sigma)$, this is equivalent to the conjunction of \begin{align*} \eta \in K,\quad \eta \cap \sigma = \varnothing,\quad \eta \cup \sigma \in K, \end{align*} \begin{align*} \eta \cap \tau = \varnothing, \end{align*} and \begin{align*} \eta \cup \tau \in K,\quad (\eta \cup \tau) \cap \sigma = \varnothing,\quad \eta \cup \tau \cup \sigma \in K. \end{align*} Since $\tau \cap \sigma = \varnothing$, the disjointness conditions are equivalent to \begin{align*} \eta \cap (\sigma \cup \tau)=\varnothing. \end{align*} The membership condition $\eta \cup \tau \cup \sigma \in K$ is exactly \begin{align*} \eta \cup (\sigma \cup \tau) \in K. \end{align*} Thus the defining conditions reduce precisely to \begin{align*} \eta \in K,\quad \eta \cap (\sigma \cup \tau)=\varnothing,\quad \eta \cup (\sigma \cup \tau) \in K. \end{align*} These are the defining conditions for $\eta \in \operatorname{lk}_K(\sigma \cup \tau)$. Therefore \begin{align*} \operatorname{lk}_{\operatorname{lk}_K(\sigma)}(\tau)=\operatorname{lk}_K(\sigma \cup \tau). \end{align*} This completes the proof. [/step]