[proofplan] The proof uses two nested compactness arguments. For each pair of points $(x, y)$, the strong separation hypothesis directly provides an element of $\mathcal{L}$ matching any prescribed pair of values — in particular matching $f$. For a fixed $x$, taking pointwise minima over finitely many such functions (chosen by compactness) produces an element of $\mathcal{L}$ that agrees with $f$ at $x$ and is everywhere less than $f + \varepsilon$. Then taking pointwise maxima over finitely many $x$-values (again by compactness) produces an element within $\varepsilon$ of $f$ uniformly. No algebraic structure is needed — only the lattice operations and the separation hypothesis. [/proofplan] [step:For each pair $(x,y)$, the strong separation hypothesis gives $g_{xy} \in \mathcal{L}$ with $g_{xy}(x) = f(x)$ and $g_{xy}(y) = f(y)$] Let $f \in C(K; \mathbb{R})$ and fix distinct points $x, y \in K$. The strong separation hypothesis states that for every pair of real numbers $\alpha, \beta$, there exists $h \in \mathcal{L}$ with $h(x) = \alpha$ and $h(y) = \beta$. Applying this with $\alpha = f(x)$ and $\beta = f(y)$, we obtain $g_{xy} \in \mathcal{L}$ with \begin{align*} g_{xy}(x) = f(x), \qquad g_{xy}(y) = f(y). \end{align*} For the case $x = y$, we set $g_{xx} := g$ for any $g \in \mathcal{L}$ satisfying $g(x) = f(x)$ (which exists by strong separation applied with any $y' \neq x$, $\alpha = f(x)$, $\beta$ arbitrary). [guided] The strong separation hypothesis is strictly stronger than the separation hypothesis in the algebra version of Stone--Weierstrass. There, $\mathcal{A}$ separates points (meaning there exists $h$ with $h(x) \neq h(y)$), and additional work is needed to prescribe exact values. Here, the strong separation gives us exact interpolation at two points for free. This stronger hypothesis is necessary because a lattice (unlike an algebra) does not admit scalar multiplication or addition of constants. We cannot "rescale and shift" a separating function to match prescribed values. [/guided] [/step] [step:Fix $x$ and use $\min$ over finitely many functions to approximate $f$ from above] Fix $x \in K$ and $\varepsilon > 0$. For each $y \in K$, the function $g_{xy} \in \mathcal{L}$ satisfies $g_{xy}(y) = f(y)$, so the set \begin{align*} V_y := \{z \in K : g_{xy}(z) < f(z) + \varepsilon\} \end{align*} is open (as the preimage of $(-\infty, \varepsilon)$ under the continuous function $g_{xy} - f$) and contains $y$ (since $g_{xy}(y) - f(y) = 0 < \varepsilon$). The collection $\{V_y\}_{y \in K}$ is an open cover of $K$. Since $K$ is compact, there exist finitely many points $y_1, \ldots, y_m \in K$ with $K = V_{y_1} \cup \cdots \cup V_{y_m}$. Define \begin{align*} h_x := \min(g_{x y_1}, g_{x y_2}, \ldots, g_{x y_m}). \end{align*} Since $\mathcal{L}$ is closed under $\min$ and $m$ is finite, $h_x \in \mathcal{L}$ (applying $\min$ iteratively: $\min(g_{xy_1}, g_{xy_2}) \in \mathcal{L}$, then $\min(\min(g_{xy_1}, g_{xy_2}), g_{xy_3}) \in \mathcal{L}$, etc.). The function $h_x$ satisfies: - $h_x(x) = \min_j g_{xy_j}(x) = \min_j f(x) = f(x)$, since $g_{xy_j}(x) = f(x)$ for every $j$. - $h_x(z) < f(z) + \varepsilon$ for all $z \in K$: each $z$ belongs to some $V_{y_j}$, where $g_{xy_j}(z) < f(z) + \varepsilon$, and $h_x(z) \leq g_{xy_j}(z)$. [guided] The minimum of finitely many continuous functions, each bounded above by $f + \varepsilon$ in some open neighbourhood, is globally bounded above by $f + \varepsilon$. The compactness of $K$ is essential to reduce to finitely many functions — an infinite minimum need not be continuous and need not belong to $\mathcal{L}$. At the point $x$, all the functions being minimised agree (they all equal $f(x)$), so the minimum also equals $f(x)$. Away from $x$, the minimum pulls the approximation down toward $f$, preventing any single $g_{xy_j}$ from overshooting by more than $\varepsilon$. [/guided] [/step] [step:Use $\max$ over finitely many $x$-values to approximate $f$ from below and complete the proof] For each $x \in K$, the function $h_x \in \mathcal{L}$ satisfies $h_x(x) = f(x)$ and $h_x < f + \varepsilon$ on all of $K$. Since $h_x(x) = f(x) > f(x) - \varepsilon$, the set \begin{align*} U_x := \{z \in K : h_x(z) > f(z) - \varepsilon\} \end{align*} is open (preimage of $(-\varepsilon, \infty)$ under $h_x - f$) and contains $x$. The collection $\{U_x\}_{x \in K}$ covers $K$, so by compactness there exist $x_1, \ldots, x_\ell \in K$ with $K = U_{x_1} \cup \cdots \cup U_{x_\ell}$. Define \begin{align*} h := \max(h_{x_1}, h_{x_2}, \ldots, h_{x_\ell}) \in \mathcal{L}. \end{align*} For every $z \in K$: - **Lower bound:** There exists $i$ with $z \in U_{x_i}$, so $h(z) \geq h_{x_i}(z) > f(z) - \varepsilon$. - **Upper bound:** For every $i$, $h_{x_i}(z) < f(z) + \varepsilon$, so $h(z) = \max_i h_{x_i}(z) < f(z) + \varepsilon$. Therefore $\|h - f\|_\infty < \varepsilon$. Since $h \in \mathcal{L}$ and $\varepsilon > 0$ was arbitrary, $f \in \overline{\mathcal{L}}$. As $f \in C(K; \mathbb{R})$ was arbitrary, $\overline{\mathcal{L}} = C(K; \mathbb{R})$. [/step]