Smooth weak Dirichlet solutions are classical

Every Sobolev order. Fix $m\in \mathbb{N}$. Since $a^{ij},b^i,c$ and $f$ extend smoothly to a neighbourhood of $\bar{\mathrm{\Omega }}$, their restrictions to $\mathrm{\Omega }$ are of class $C^{\mathrm{\infty }}(\mathrm{\Omega })$ with bounded derivatives of every order on $\mathrm{\Omega }$, and $f\in H^m(\mathrm{\Omega })$; [F1] with $k=m$ gives $u\in H^{m+2}(\mathrm{\Omega })$. As $m$ was arbitrary, $u\in H^m(\mathrm{\Omega })$ for every $m$.

A smooth representative up to the boundary. Fix $\mathrm{\ell }\in \mathbb{N}$ and choose $m>\mathrm{\ell }+n\mathrm{/}2$. By step 1.1, $u\in H^m(\mathrm{\Omega })$, and [F2] gives a representative of $u$ whose derivatives up to order $\mathrm{\ell }$ are continuous on $\bar{\mathrm{\Omega }}$; these representatives are compatible for different $\mathrm{\ell }$ (they are weak derivatives of one another on $\mathrm{\Omega }$ and continuous), so they determine a function $\tilde{u}\in C^{\mathrm{\infty }}(\bar{\mathrm{\Omega }})$ with $\tilde{u}=u$ a.e. on $\mathrm{\Omega }$.

The equation pointwise. Since $u\in H^2(\mathrm{\Omega })$, the strong form $Lu=f$ holds a.e. on $\mathrm{\Omega }$ with the a.e. expression $(D_i{a}^{ij})D_{j}u+a^{ij}{D}_i{D}_{j}u$; both sides are continuous functions on $\mathrm{\Omega }$ for the representative $\tilde{u}$ and the smooth data, and continuous functions agreeing a.e. agree everywhere, so $L\tilde{u}=f$ pointwise in $\mathrm{\Omega }$.

Boundary values. The class $u$ lies in $H_0^1(\mathrm{\Omega })$, so its trace vanishes; on the other hand the trace of a Sobolev class with a continuous representative equals the restriction of that representative, so the restriction of $\tilde{u}$ is zero surface-almost-everywhere. If it were nonzero at a boundary point, continuity would make it nonzero on a relatively open boundary patch, which has positive surface measure by the boundary graph parametrization. Hence $\tilde{u}{\mathrm{\mid }}_{\mathrm{\partial }\mathrm{\Omega }}=0$ at every boundary point.

Conclusion. Under $C^{\mathrm{\infty }}$ boundary regularity and $C^{\mathrm{\infty }}$ data extending to the closure, the weak zero-trace solution is the Sobolev class of a function $\tilde{u}\in C^{\mathrm{\infty }}(\bar{\mathrm{\Omega }})$ that solves the equation pointwise and vanishes on the boundary; the Axiom of Choice enters through the embedding and trace interfaces of [F2] and [F3], and Countable Choice through the Sobolev interfaces of [F1].