Splitting field of a separable polynomial is separable
New Answer
[New version of the new answer. Thank you very much to KCd! --- See his comment.]
The simplest, I think, is to prove the Fundamental Theorem of Galois Theory (FTGT) for a normal extension $E/F$ generated by finitely many separable elements, and to obtain the fact that all the elements of $E$ are separable over $F$ as a corollary.
The point is that the FTGT can be given a very short proof, which will be described below. (I of course believe that this proof is complete. Thanks for correcting me if I'm wrong.)
FTGT (Fundamental Theorem of Galois Theory). Let $F$ be a field, let $A$ be an algebraic closure of $F$, let $p\in F[X]$ be a product of separable irreducible polynomials, let $E$ be a splitting field for $p$ over $F$, and let $a_1,\dots,a_n$ be the roots of $p$ in $E$. Then
the group $G$ of $F$-automorphisms of $E/F$ is finite,
there is a bijective correspondence between the sub-extensions $S/F$ of $E/F$ and the subgroups $H$ of $G$, and we have $$ S\leftrightarrow H\iff H=\text{Aut}_S E\iff S=E^H\implies[E:S]=|H|, $$ where $E^H$ is the fixed subfield of $H$, where $[E:S]$ is the degree (that is the dimension) of $E$ over $S$, and where $|H|$ is the order of $H$.
We are taking for granted
$(1)$ the universal property of a simple algebraic extension, and
$(2)$ the existence and universal property of our splitting field $E$,
which we briefly recall:
$(1)$ If $a$ is algebraic over a field $K$, then the $K$-embeddings of $K(a)$ in an extension $L$ of $K$ are in natural bijection with the roots in $L$ of the minimal polynomial of $a$ over $K$.
$(2)$ Any root of $p$ in any extension of $E$ is in $E$, and $E$ is generated over $F$ by the roots $a_i$ of $p$. Moreover, if $S/F$ is a sub-extension of $E/F$, then any $F$-embedding of $S$ in $E$ extends to an $F$-automorphism of $E$.
Going back to the assumptions of the FTGT, we claim:
$(3)$ If $S/F$ is a sub-extension of $E/F$, then $[E:S]=|\text{Aut}_S E|$.
$(4)$ If $H$ is a subgroup of $G$, then $|H|=[E:E^H]$.
Proof that (3) and (4) imply the FTGT. Let $S/F$ be a sub-extension of $E/F$ and put $H:=\text{Aut}_S E$. Then we have trivially $S\subset E^H$, and $(3)$ and $(4)$ imply $$ [E:S]=[E:E^H]. $$ Conversely let $H$ be a subgroup of $G$ and set $\overline H:=\text{Aut}_{E^H}E$. Then we have trivially $H\subset\overline H$, and $(3)$ and $(4)$ imply $|H|=|\overline H|$.
To prove that any element $a$ of $E$ is separable over $F$, put $H:=\text{Aut}_{F(a)}E$, and note that the set of $F$-embeddings of $F(a)$ in $E$ is in natural bijection with the set $G/H$, whose cardinality is, by the FTGT, equal to $[F(a):F]$.
Proof of (3). The statement follows from the fact that any $F$-embedding of $S_i:=S(a_1,\dots,a_i)$ in $E$ has exactly $[S_{i+1}:S_i]$ extensions to $S_{i+1}$.
Proof of (4). In view of (3) it is enough to check $|H|\ge[E:E^H]$. Let $k$ be an integer larger than $|H|$, and pick a $$ b=(b_1,\dots,b_k)\in E^k. $$ We must show that the $b_i$ are linearly dependent over $E^H$, or equivalently that $b^\perp\cap(E^H)^k$ is nonzero, where $?^\perp$ denotes the vectors orthogonal to ? in $E^k$ with respect to the dot product on $E^k$. Any element of $b^\perp \cap (E^H)^k$ is necessarily orthogonal to $h(b)$ for any $h \in H$, so $b^\perp \cap (E^H)^k = (Hb)^\perp \cap (E^H)^k$, where $Hb$ is the $H$-orbit of $H$. We will show $(Hb)^\perp \cap (E^H)^k$ is nonzero. Since the span of $Hb$ in $E^k$ has $E$-dimension at most $|H| < k$, $(Hb)^\perp$ is nonzero. Choose a nonzero vector $x$ in $(Hb)^\perp$ such that $x_i=0$ for the largest number of $i$ as possible among all nonzero vectors in $(Hb)^\perp$. Some coordinate $x_j$ is nonzero in $E$, so by scaling we can assume $x_j = 1$ for some $j$. Since the subspace $(Hb)^\perp$ in $E^k$ is stable under the action of $H$, for any $h$ in $H$ we have $h(x) \in (Hb)^\perp$, so $h(x)-x \in (Hb)^\perp$. Since $x_j = 1$, the $j$-th coordinate of $h(x) - x$ is $0$, so $h(x)-x = 0$ by the choice of $x$. Since this holds for all $h$ in $H$, $x$ is in $(E^H)^k$.
Old Answer
This is more a hint than an answer. I think the key point here is to understand the equivalence between various definitions of a separable extension. I'll just try to emphasize some of the basic facts.
Let $K$ be a field, $A/K$ an algebraic closure, and $L/K$ an extension of degree $d < \infty$ contained in $A$. We claim that the following conditions are equivalent:
(1) $L/K$ is generated by separable elements,
(2) each element of $L$ is separable over $K$,
(3) there are exactly $d$ embeddings of $L$ in $A$ over $K$.
We say that $L/K$ is separable if it satisfies these conditions. Let's sketch a proof of the equivalence.
Say that the number, denoted by $[L:K]_s$, of $K$-embeddings of $L$ in $A$ is the separable degree of $L/K$.
Let $M$ be a finite degree extension of $K$ contained in $A$, and $L$ a field between $K$ and $M$. We claim:
(4) $[M:K]_s=[M:L]_s\ [L:K]_s$.
This is an easy, but instructive, exercise.
Claim: (1) and (3) are equivalent when $K$ is generated by a single element $\alpha$. Indeed, if $f\in K[X]$ is the minimal polynomial of $\alpha$, then $[L:K]$ is the degree of $f$, whereas $[L:K]_s$ is the number of distinct roots of $f$ in $A$.
In view of (4), the above claim implies that (1), (2) and (3) are equivalent in the general case.
As a corollary, we see that a finite degree extension $L/K$ contains a largest separable sub-extension $S$, and that $[S:K]=[L:K]_s$.
As a corollary to the corollary, we get the fact suggested by the notation that the integer $[L:K]_s$ does not depend on the choice of an algebraic closure of $L$.
$\DeclareMathOperator{\aut}{Aut}$ $\newcommand{\vp}{\varphi}$Here is a short proof.
Let $E$ be the splitting field of a separable polynomial $p(x)$ over a field $F$. We need to show that $E:F$ is a separable extension.
Claim 1. $[E:F]=|\aut(E:F)|$.
Proof. Say $\deg p=n$ and let $a_1, \ldots, a_n$ be all the roots of $p$ in $E$. Write $F_i$ to denote $F(a_1, \ldots, a_i)$. We will show that each $F$-embedding of $F_i$ in $E$ admits exactly $[F_{i+1}:F_i]$ extensions to an embedding of $F_{i+1}$ into $E$.
Suppose $\vp:F_i\to E$ be an $F$-embedding of $F_i$ in $E$ and let $d_i=[F_{i+1}:F_i]$. We need to show that there are exactly $d_i$ different extensions of $\vp$ to an embedding of $F_{i+1}$ into $E$. Let $p_i(x)\in F_i[x]$ be the minimal polynomial of $a_i$ over $F_i$. Since $p_i$ and $p$ both have $a_{i+1}$ has a root, we have $p_i|p$ and therefore $p_i$ has $d_i$ distinct roots in $E$. Now we may extend $\vp$ to $F_{i+1}$ by sending $a_{i+1}$ to any root of $p_i$ we wish. Further, all extensions of $\vp$ send $a_{i+1}$ to some root of $p_i$. Lastly, any extension of $\vp$ is determined completely by its action on $a_{i+1}$. Therefore there are precisely $d_i=[F_{i+1}:F_i]$ different extensions of $\vp$ to $F_{i+1}$.
Thus there are at least $[F_n:F_{n-1}]\cdots [F_1:F]=[E:F]$ distinct elements in $\aut(E:F)$. There cannot be any more and thus we are done. $\blacksquare$
Claim 2. The fixed field in $E$ of $\aut(E:F)$ is $F$.
Proof. Let $M$ be the fixed field of $\aut(E:F)$. Thus there is a natural bijection between $\aut(E:M)$ and $\aut(E:F)$. Note that $p(x)$ is a separable polynomial over $M$ whose splitting field is $E$. Therefore, by Claim 1, we have $|\aut(E:M)|=[E:M]$. This shows that $|\aut(E:F)|=[E:M]$. In the light of Claim 1, this is only possible if $M=F$. $\blacksquare$
Claim 3. $E$ is separable over $F$.
Proof. Let $\alpha\in E$ be chosen arbitrarily and $f(x)$ be the minimal polynomial of $\alpha$ over $F$. We need to show that $f(x)$ is separable over $F$. Note that $E$ is normal over $F$ and therefore completely splits $f$. Write $f=(x-\beta_1)^{r_1}\cdots (x-\beta_k)^{r_k}$ in $E[x]$, where $\beta_i$'s are pairwise distinct. If $\vp\in \aut(E:F)$, then we see that
$$f=(x-\beta_1)^{r_1}\cdots (x-\beta_k)^{r_k}= (x-\vp(\beta_1))^{r_1}\cdots (x-\vp(\beta_k))^{r_k}$$
which lets us conclude that $\vp$ permutes $\{\beta_1, \ldots, \beta _k\}$. Since $\vp$ was arbitrary in $\aut(E:F)$, we conclude that $\aut(E:F)$ acts on $\{\beta_1, \ldots, \beta_k\}$. Therefore the symmetric functions on $\beta_i$'s remain fixed by $\aut(E:F)$. Applying Claim 2, we see that each symmetric function in $\beta_i$'s is a member of $F$. Therefore the polynomial $(x-\beta_1)\cdots (x-\beta_k)$ is in $F[x]$. Since $f(x)$ was irreducible over $F$, we are forced to have $f(x)=(x-\beta_1)\cdots (x-\beta_k)$ and we have shown that $\alpha$ is separable over $F$. $\blacksquare$