Corollary 2 (Mac Lane)

— Let $K$ be an algebraic closure of $K$ and $K^{p^{-\infty}}$ the perfect closure of $K$ in $\overline{K}$. For a subextension $E$ of $\overline{K}$ to be separable over $K$ it is necessary and sufficient that it should be linearly disjoint from $K^{p^{-\infty}}$ over $K$.

We can immediately reduce to the case where $[E : K]$ is finite. Let $(x_i)_i$, be a basis of $E$ over $K$. For $E$ to be linearly disjoint from $K^{p^{-\infty}}$ it is necessary and sufficient that it should be so from $K^{p^n}$ for all $n \geq 0$, and this just means that the relation $\sum_{i \in I} x_i a_i^{p^{-n}} = 0$ implies $a_i = 0$ for all $i \in I$, for any family $(a_i)_i$, of elements of $K$. This in turn means that the family $(x_i^{p^n})_{i \in I}$ is free over $K$, or also that it is a basis of the vector space $E$ over $K$. Put differently, $E$ is linearly disjoint from $K^{p^{-n}}$ if and only if $E = K(E^{p^n})$. Now it suffices to apply Prop. 11.