Intersection of two subgroups of finite index is finite

Today's idea came from someone anonymous at math.stackexchange.com. We'll be seeing, with an interesting group action, why the intersection of two subgroups of finite index is finite.

Let $(G, +)$ be a group, and $H$ and $K$ subgroups. Let $G/H$ and $G/K$ be the sets of left cosets of $H$ and $K$, respectively. Consider the diagonal action of $G$ on $G/H \times G/K$.

(In other words, $g$ acting on $(g' + H, g'' + K)$ is $((g + g') + H, (g + g'') + K)$. One can quickly check this is a well-defined group action.)

The stabilizer of $H\times K$ is the set of all $g \in G$ such that $g + H = H$ and $g + K = K$, so the stabilizer of $H \times K$ is $H \cap K$.

Now we suppose $H$ and $K$ are subgroups of finite index. Then the orbit of $H \times K$ has to be finite, since $G/H \times G/K$ is finite. By the orbit stabilizer theorem, it follows that $[G : H \cap K]$ is finite.