The RMK functional outer content is an outer measure

The definition gives ${\mu }^{\ast }(\mathrm{\varnothing })=0$ and monotonicity: an open superset of $F$ is also one of $E$ when $E\subseteq F$.

For any sequence of open sets $(U_n{)}_{n\ge 0}$ put $U={\bigcup }_n{U}_n$. [L0, L1] Use the equivalent supremum in [L0], not merely the condition $f\le {\mathbf{1}}_U$. For $f\prec U$, its compact support $K$ is contained in $U$. If $K$ is empty, $f=0$. Otherwise a finite set of distinct indices $n_1,\dots ,n_m$ gives a cover of $K$. By [L1] choose nonnegative ${\phi }_j\in C_c(X)$ with support contained in $U_{n_j}$ and sum $1$ near $K$. Then $f={\sum }_{j}f{\phi }_j$. On $K$ each ${\phi }_j\le 1$; off $K$ the product is zero. Thus $0\le f{\phi }_j\le 1$ and its compact support is contained in $U_{n_j}$, so $f{\phi }_j\prec U_{n_j}$. Linearity gives $\mathrm{\Lambda }(f)\le {\sum }_{j=1}^m\rho (U_{n_j})\le {\sum }_{n\ge 0}\rho (U_n)\mathrm{.}$ The last inequality uses the distinct indices and nonnegativity. Taking the supremum in [L0] proves countable subadditivity for these open sets.

Let $E\subseteq {\bigcup }_{n\ge 0}{E}_n$. [given, L2, step 1.2] If ${\sum }_n{\mu }^{\ast }(E_n)=\mathrm{\infty }$, the required inequality is automatic. Otherwise fix $\epsilon >0$. Each set of open supersets $U_n$ of $E_n$ satisfying $\rho (U_n)<{\mu }^{\ast }(E_n)+\epsilon 2^{-n-1}$ is nonempty by the defining infimum. To select all $U_n$, consider the set of finite lists of admissible choices, starting with the empty list, with relation given by one-term extension. Every list has an extension. Applying [L2] and taking the union of the resulting coherent lists supplies the sequence. This is the countable selection used here; [L0] and [L1] also use the stated DC hypothesis. No implication theorem from a later choice page is assumed. For $U={\bigcup }_n{U}_n$, step 1.2 now gives ${\mu }^{\ast }(E)\le \rho (U)\le {\sum }_n\rho (U_n)\le {\sum }_n{\mu }^{\ast }(E_n)+\epsilon \mathrm{.}$ Letting $\epsilon \downarrow 0$ completes countable subadditivity.