Neat submanifolds have boundary-adapted slice charts

If $p\in \mathrm{Int}S$, then [L1] puts $p$ in $\mathrm{Int}M$, and [L2] applies inside $\mathrm{Int}M$. Now let $p\in \mathrm{\partial }S=S\cap \mathrm{\partial }M$. Choose boundary coordinates $(u,s)$ on $S$ and $(z,t)$ on $M$, and write the inclusion as $F(u,s)=(G(u,s),h(u,s))$. By [L1], $h(u,0)=0$ and transversality gives $d(h{\mathrm{\mid }}_S{)}_p\mathrm{\ne }0$. Its derivatives in the $u$-directions vanish on the face, so ${\mathrm{\partial }}_{s}h(p)\mathrm{\ne }0$; it is positive because $h(u,s)\ge 0$ for $s\ge 0$.

By [L3], replacing the source normal coordinate $s$ by $h(u,s)$ is a half-space-preserving local coordinate change. Thus assume $F(u,s)=(G(u,s),s)$. The restriction of $F$ to the face is an embedding, so $D_{u}G(u,0)$ has rank $k-1$. If $k>1$, choose an invertible $(k-1)\times (k-1)$ minor and use [L3] again in a coordinate change preserving $s$; if $k=1$, this change is empty. In either case $F(u,s)=(u,H(u,s),s)$, where $H$ has $n-k$ components.

The target coordinate change $(z^{\mathrm{\prime }},z^{\mathrm{\prime }\mathrm{\prime }},t)⟼(z^{\mathrm{\prime }},z^{\mathrm{\prime }\mathrm{\prime }}-H(z^{\mathrm{\prime }},t),t)$ is a half-space-preserving local diffeomorphism, with inverse obtained by adding $H(z^{\mathrm{\prime }},t)$. It sends $S$ to the coordinate half-slice $\{z^{\mathrm{\prime }\mathrm{\prime }}=0,t\ge 0\}$ and sends $S\cap \mathrm{\partial }M$ to its face $\{z^{\mathrm{\prime }\mathrm{\prime }}=0,t=0\}$. This proves the simultaneous straightening and the asserted equality of induced boundary structures.