@Lucas the standard proof for the primitive element theorem is the one that @Balarka mentioned. There's another proof. By Galois theory (passing to the normal closure of the extension), a finite separable extension has only finitely many subextensions. Now if the ground field is infinite, then a theorem in linear algebra says that a vector space is not the union of finitely many proper subspaces.
Thus one can choose any element not contained in any proper subextension and this will automatically be a primitive element.

if $E/K$ is separable with $[E:K]=n$ and $\overline{K}$ is an algebraic closure, then $\overline{K} \otimes_K E \cong \overline{K}^n$ (as algebras). So if $E/L/K$ is a subextension with $[L:K]=m$, then tensoring the inclusion $L \hookrightarrow E$ gives an injection of $\overline{K}$-algebras $\overline{K} \otimes_K L \hookrightarrow \overline{K} \otimes_K E$, but since $\overline{K} \otimes_K L \cong \overline{K}^m$, it is a subalgebra generated by idempotents,
but there are only finitely many idempotents in $\overline{K} \otimes_K E \cong \overline{K}^n$, all components have to be $1$ or $0$