[proofplan] The proof is an order-theoretic unpacking of the definition of sequential relaxation. Constant sequences give admissible competitors in the defining infimum for $\overline F$, which proves $\overline F\le F$. Conversely, every sequence in $X$ has all of its energy values bounded below by $\inf_X F$, so every admissible liminf in the definition of $\overline F$ is bounded below by the same number. The recovery-sequence assertion then follows by substituting the equality $\overline F(u)=\inf_X F$ into the assumed convergence of $F(u_k)$. [/proofplan] [step:Use constant sequences to compare the relaxation with the original functional] Fix $u\in X$, and write $\mathbb N=\{1,2,3,\dots\}$. Define the sequence $(c_k)_{k=1}^{\infty}\subset X$ by $c_k=u$ for every $k\in\mathbb N$. By the hypothesis on the convergence structure, $c_k\to u$. Hence this sequence is admissible in the defining infimum for $\overline F(u)$, and therefore $\overline F(u)\le \liminf_{k\to\infty}F(c_k)=F(u)$. Since $u\in X$ was arbitrary, $\overline F\le F$ on $X$. [guided] Fix a point $u\in X$. To compare $\overline F(u)$ with $F(u)$, we need to produce one admissible sequence in the definition of $\overline F(u)$. Define the constant sequence $(c_k)_{k=1}^{\infty}\subset X$ by $c_k=u$ for every $k\in\mathbb N$. The convergence structure was assumed to make constant sequences converge to their constant values, so $c_k\to u$. Thus $(c_k)$ belongs to the family of sequences over which the infimum defining $\overline F(u)$ is taken. Here $\mathbb N=\{1,2,3,\dots\}$ is the index set for the sequence. The energy values along this sequence are also constant: $F(c_k)=F(u)$ for every $k\in\mathbb N$. Therefore $\liminf_{k\to\infty}F(c_k)=F(u)$. Since an infimum is bounded above by each admissible value, the definition of $\overline F(u)$ gives $\overline F(u)\le F(u)$. Because the point $u\in X$ was arbitrary, this proves $\overline F\le F$ on all of $X$. [/guided] [/step] [step:Bound every relaxed value from below by the original infimum] Let $m=\inf_{v\in X}F(v)$ with values in $[-\infty,\infty]$. If $X=\varnothing$, then both infima in the theorem are $+\infty$ by convention, and the equality of infima follows. Assume now that $X\neq\varnothing$. Fix $u\in X$, and let $(u_k)_{k=1}^{\infty}\subset X$ be any sequence such that $u_k\to u$. Since $m$ is the infimum of $F$ over $X$, each term satisfies $m\le F(u_k)$. Taking the lower limit preserves this lower bound, so $m\le \liminf_{k\to\infty}F(u_k)$. Taking the infimum over all sequences converging to $u$ gives $m\le \overline F(u)$. Thus $m$ is a lower bound for $\overline F$ on $X$, and hence $\inf_{u\in X}F(u)=m\le \inf_{u\in X}\overline F(u)$. [/step] [step:Take infima to prove equality] From $\overline F(u)\le F(u)$ for every $u\in X$, taking infima over $X$ gives $\inf_{u\in X}\overline F(u)\le \inf_{u\in X}F(u)$. The previous step gives the reverse inequality, $\inf_{u\in X}F(u)\le \inf_{u\in X}\overline F(u)$. Combining the two inequalities yields $\inf_{u\in X}\overline F(u)=\inf_{u\in X}F(u)$. [/step] [step:Identify a recovery sequence at a relaxed minimizer as a minimizing sequence] Let $u\in X$ satisfy $\overline F(u)=\inf_{v\in X}F(v)$. Let $(u_k)_{k=1}^{\infty}\subset X$ be a recovery sequence for $u$, so that $u_k\to u$ and $F(u_k)\to \overline F(u)$ in the extended-real sense. Substituting the displayed equality gives $F(u_k)\to \inf_{v\in X}F(v)$. This is exactly the defining condition that $(u_k)_{k=1}^{\infty}$ is a minimizing sequence for $F$. This proves the final assertion and completes the proof. [/step]