Solution (source code)

= Solution

Fix $a\in L$. In the ambient universe, <Separation> forms the set
$$
S=\{x\in\mathcal P(a):x\in L\}.
$$
It is a set of constructible sets, so the previous part gives an <ordinal> bound on all its members. Increase the bound to a level $L_\beta$ also containing $a$. <Transitivity> ensures $a\subseteq L_\beta$. Then
$$
S=\{x\in L_\beta:x\subseteq a\}.
$$
The inclusion test is absolute for the transitive level $L_\beta$, since all members of $x$ and $a$ lie there. The right side is consequently a subset definable over $L_\beta$ with parameter $a$, so
$$
\boxed{S\in\operatorname{Def}(L_\beta)=L_{\beta+1}\subseteq L.}
$$
For $x\in L$, transitivity of the <constructible universe> makes internal and ambient subsethood of $a$ agree. Hence $L$ satisfies that $S$ consists exactly of all its subsets of $a$. This is the <Power set> Axiom in $\langle L,\in\rangle$. It is not the assertion that every ambient subset of $a$ belongs to $L$.