Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume

Given: A natural number $n\ge 1$, the Axiom of Countable Choice, the premeasure ${\mu }_0$ on the algebra ${\mathcal{E}}_n$, and its induced outer set function ${\lambda }_n^{\ast }$.

${\lambda }_n^{\ast }$ is the outer set function induced by the premeasure ${\mu }_0$ on the algebra ${\mathcal{E}}_n$ of elementary sets (Lebesgue outer measure on ${\mathbb{R}}^n$).

Elementary volume ${\mu }_0$ is a sigma-finite premeasure on ${\mathcal{E}}_n$ (Elementary volume is a sigma-finite premeasure on the algebra of elementary sets).

Assume the Axiom of Countable Choice. The outer set function induced by a premeasure is an outer measure (Assuming countable choice, the outer set function induced by a premeasure is an outer measure).

For every $A\in {\mathcal{A}}_0$, the outer measure induced by a premeasure satisfies ${\mu }^{\ast }(A)={\mu }_0(A)$ (The induced outer measure agrees with the premeasure on the source algebra).

An outer measure on a set $X$ is a function ${\mu }^{\ast }:\mathcal{P}(X)\to [0,+\mathrm{\infty }]$ that vanishes at the empty set, is monotone, and is countably subadditive (Outer measures).

The Axiom of Countable Choice says that for every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that $f(n)\in X_n$ for every $n\in \mathbb{N}$ (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)).