Following the proof given in Milnor's Topology From A Differentiable Viewpoint:
$\require{AMScd}$
$\begin{CD}
x \in U \subseteq M @>F>> c \in V \subseteq N \\
@V\phi VV @VV\psi V \\
\phi\left(U\right) \subseteq H^{m} @>>\psi F \phi^{-1}> \psi\left(c\right) \in \psi\left(V\right)
\end{CD}$
Because $c \in N$ is a regular value of $F$, for every $x \in F^{-1}\left(c\right) \subseteq M$, there are charts $\left(U,\phi\right)$ at $x$ in $M$ and $\left(V,\psi\right)$ at $c$ in $N$ such that $\psi F \phi^{-1}: \phi\left(U\right) \subseteq H^{m} \to \psi\left(V\right) \subseteq \mathbb{R}^{n}$ is smooth, and has a regular value at $\psi\left(c\right)$.
$\begin{CD}
\phi\left(U\right) \subset W \subseteq \mathbb{R}^{m} @>G>> \psi\left(c\right) \in \mathbb{R}^{n}
\end{CD}$
Let $W$ be an open subset of $\mathbb{R}^{m}$ such that $W \cap H^{m} = \phi\left(U\right)$; and let $G:W\to\mathbb{R}^{n}$ be the smooth extension of $\psi F \phi^{-1}$ over $W$. Now, we can always choose $W$ small enough so that $G^{-1}\left(\psi\left(c\right)\right)$ does not contain any critical points (Sard's lemma; $\mathbb{R}^{m}$ is regular). Thus, $\psi\left(c\right)$ is a regular value of $G$; and by preimage theorem (for smooth manifolds), $Z := G^{-1}\left(\psi\left(c\right)\right)$ is a (m-n)-dimensional submanifold of $\mathbb{R}^{m}$.
Furthermore, since $G$ is constant over $Z$, $T_{a}Z \subseteq ker\left\{DG\left(a\right)\right\}$ for every $a \in Z$. But $DG\left(a\right):\mathbb{R}^{m}\to\mathbb{R}^{n}$ is surjective, and the rank-nullity theorem implies $dim \left(ker\left\{DG\left(a\right)\right\}\right) =$ (m-n). Thus, $T_{a}Z = ker\left\{DG\left(a\right)\right\}$.
Now, define $\pi: Z \subseteq \mathbb{R}^{m} \to \mathbb{R}$ as $\left(x_{1},\ldots,x_{m}\right) \mapsto x_{m}$.
To show that $0 \in \mathbb{R}$ is a regular value of $\pi$:
Suppose otherwise. That is, suppose $\exists$ $a \in Z \cap \partial H^{m}$ such that $d\pi_{a}:T_{a}Z \to \mathbb{R}$ is not surjective. Then, $ker \left\{d\pi_{a}\right\}$ $=$ $T_{a}Z$ $=$ $ker \left\{DG(a)\right\}$. But, we know that $ker \left\{d\pi_{a}\right\} \subseteq \mathbb{R}^{m-1} \times \left\{0\right\} = \partial H^{m}$. Thus, $ker \left\{DG(a)\right\} \subseteq \partial H^{m}$ if $0$ is not a regular value for $\pi$.
Now, since $c \in N$ is a regular value of $F|_{\partial M}$ as well, arguing as before, we can show that $\bar{G} := G|_{W\cap\partial H^{m}}$ has a regular value at $\psi\left(c\right)$. That is, for every $a \in Z\cap\partial H^{m}$, $D\bar{G}\left(a\right): \mathbb{R}^{m-1} \to \mathbb{R}^{n}$ is surjective; and by rank-nullity theorem, $dim \left(ker\left\{D\bar{G}\left(a\right)\right\}\right) = $ (m-n-1)
Finally, $ker \left\{DG(a)\right\} \subseteq \partial H^{m}$ implies $ker \left\{DG(a)\right\} = ker \left\{D\bar{G}(a)\right\}$, which is clearly false (dimension mismatch). Hence, $0$ must be a regular value for $\pi$.
Since $0 \in \mathbb{R}$ is a regular value for $\pi$, $\left\{z \in Z | \pi\left(z\right) \geq 0\right\}$ $=$ $\phi\left(U \cap F^{-1}\left(c\right)\right)$ is a manifold with boundary $\left\{z \in Z | \pi\left(z\right) = 0\right\}$ $=$ $\phi\left(U \cap F^{-1}\left(c\right) \cap \partial M \right)$.
$\phi$ being a diffeomorphism, $U \cap F^{-1}\left(c\right)$ is a manifold with boundary $U \cap F^{-1}\left(c\right) \cap \partial M$. Observing that this is true for every $x \in F^{-}\left(c\right)$ completes the proof.
First of all, you are right about assuming that do Carmo's definition could be easily generalized to submanifolds in any $\mathbb{R}^n$, or in any $M$.
The definitions are slightly different in general. Let's see why.
1) Jeffrey Lee's $\Rightarrow$ do Carmo (generalized).
Suppose $p\in S$, then there is a chart $(U,x)$ in $M$ such that $x(U\cap S)=x(U)\cap (\mathbb{R}^k \times \{0\})$, we can perform a translation in $\mathbb{R}^{n}$ ($n=$ dim $M$) to get $c=0$. Now, just identifying $\mathbb{R}^k$ and $\mathbb{R}^k \times {0}$, we have a parametrization in the sense of do Carmo: $y=x^{-1}|_V: V=x(U\cap S)\rightarrow M$ which is clearly $C^{\infty}$ and a homeomorphism onto its image (because its the restriction of a chart, which is everything good you could desire) and its domain is open in $\mathbb{R}^k$ because $x(U)$ is open in $\mathbb{R}^n$. The injectivity of its differential comes from the fact that $y \circ x|_{U \cap S}=Id_V$, now use the chain rule.
2) do Carmo's (generalized) $\Rightarrow$ Jeffrey Lee's.
Suppose you have $p\in S$, $V\subset M$ open and a map $y:U \rightarrow V\cap S$ satistying 1), 2), 3), with $U$ open subset of $\mathbb{R}^k$. You need to garantee that the map $y^{-1}|:V\cap S \rightarrow U\subset \mathbb{R}^k$ is just the restriction of a chart $(x,W)$ around $p$ in $M$. You can prove that as follows.
Since $y$ is $C^\infty$, one-one and its differential is one-one, it is a diffeomorphism onto its image (one of the implications of the Inverse Function Theorem). Now since this work is all local, and $M$ is locally $\mathbb{R}^n$, we can solve the situation in $\mathbb{R}^n$ and then translate it to $M$ without any difficulty. In these case, once the $y^{-1}$'s are diffeomorphisms from some open sets of $S$ to $\mathbb{R}^k$, you can easily construct extensions for them by just using that $\mathbb{R}^n$ splits orthogonally as $\mathbb{R}^k\times \mathbb{R}^{n-k}$, and use this locally to define a chart in an open subset of $\mathbb{R}^n$ by just sliding up and down along segments orthogonal to your open in $S$, something like $x((p,0)+t(0,v))=y(p,0)+t(0,v)$ (your open may not be contained in $\mathbb{R}^k\times 0$, but I put it like that for the sake of simplicity. I'm sure you can adjust it to work in the "general" case). This would work because in $\mathbb{R}^n$ any diffeomorphism is a chart of its structure.
To conclude, both definitions are equivalent even in the general case when your ambient is any manifold, and your surfaces are actually submanifolds.
Remark: My original answer was wrong in one implication. Full credit to @Thomas, who made me aware of my mistake.
Best Answer
Your proof is correct in addition to being good. I would like to remark that using mostly the same tools you can prove the stronger statement "Every submanifold $X\subset\mathbb{R}^n$ is locally expressible as a graph". Here's the problem spelled out in Guillemin & Pollack p.19.