Step 1: $K^{\mathrm{Gal}(K/E)} = E$ for every intermediate field $E$.

$K/E$ is Galois (normal and separable are inherited). By Artin's theorem, $K^{\mathrm{Gal}(K/E)} = E$.

Step 2: $\mathrm{Gal}(K/K^H) = H$ for every subgroup $H \leq G$.

By Artin's theorem applied to $H$ acting on $K$: $K/K^H$ is Galois with $\mathrm{Gal}(K/K^H) = H$ and $[K:K^H] = |H|$.

Step 3: The maps are mutually inverse.

From Steps 1 and 2: $E \mapsto \mathrm{Gal}(K/E) \mapsto K^{\mathrm{Gal}(K/E)} = E$ and $H \mapsto K^H \mapsto \mathrm{Gal}(K/K^H) = H$.

Step 4: Inclusion reversal. $E_1 \subseteq E_2$ implies $\mathrm{Gal}(K/E_2) \leq \mathrm{Gal}(K/E_1)$ (if $\sigma$ fixes $E_2$ pointwise, it fixes $E_1 \subseteq E_2$ pointwise).

Step 5: Degree formulas. $[K:E] = |\mathrm{Gal}(K/E)|$ by the Galois property. $[E:F] = [K:F]/[K:E] = |G|/|\mathrm{Gal}(K/E)| = [G:\mathrm{Gal}(K/E)]$.

Step 6: Normal extensions correspond to normal subgroups.

$(\Rightarrow)$: Suppose $E/F$ is normal. For any $\sigma \in G$ and $\tau \in \mathrm{Gal}(K/E)$: we need $\sigma\tau\sigma^{-1} \in \mathrm{Gal}(K/E)$, i.e., $\sigma\tau\sigma^{-1}(e) = e$ for all $e \in E$. Since $E/F$ is normal, $\sigma(E) = E$ (normality means $\sigma$ maps $E$ to itself). So $\sigma^{-1}(e) \in E$, then $\tau(\sigma^{-1}(e)) = \sigma^{-1}(e)$, then $\sigma\tau\sigma^{-1}(e) = e$. So $H = \mathrm{Gal}(K/E)$ is normal in $G$.

$(\Leftarrow)$: Suppose $H = \mathrm{Gal}(K/E) \trianglelefteq G$. For any $\sigma \in G$ and $\alpha \in E$: for all $\tau \in H$, $(\sigma^{-1}\tau\sigma)(\alpha) = \alpha$ (since $\sigma^{-1}\tau\sigma \in H$ by normality), so $\tau(\sigma(\alpha)) = \sigma(\alpha)$. Thus $\sigma(\alpha) \in K^H = E$. So $\sigma(E) \subseteq E$ for all $\sigma \in G$, meaning every $F$-embedding of $E$ into $\overline{F}$ lands in $E$, which is the definition of normality.

When $H \trianglelefteq G$: restriction gives a surjection $G \to \mathrm{Gal}(E/F)$ with kernel $H$, so $\mathrm{Gal}(E/F) \cong G/H$. $\blacksquare$