Existence of maximal tori

Consider the torus subgroups $T$ of $G$ containing $T_0$. Their dimensions form a nonempty subset of $\{0,\dots ,\dim G\}$: it contains $\dim T_0$, and an embedded submanifold has dimension at most that of its ambient manifold. This finite set has a largest member $d$, and by its definition there exists a torus $T$ containing $T_0$ with dimension $d$. Fix one such $T$.

Let $S$ be any torus of $G$ containing $T$. The inclusion $j:T\to S$ is smooth: in any submanifold chart for the embedded $S\subseteq G$, the smooth inclusion of $T$ into $G$ has zero transverse coordinates and its remaining coordinates give a smooth map into $S$. Its differential is injective because composition with the inclusion $S\to G$ is the immersion $T\to G$. Therefore $\dim T\le \dim S$. Since $S$ also contains $T_0$, maximality of $d$ gives $\dim S\le d=\dim T$; thus $d{j}_e$ is an isomorphism.

By [F2], $T$ contains an open neighborhood of $e$ in $S$. Its translates by elements of $T$ show that $T$ is open in $S$. Each other coset is also open by translation, so the complement of $T$ is open. Connectedness of $S$ and nonemptiness of $T$ force $T=S$. Consequently $T$ is a maximal torus containing $T_0$.

The trivial subgroup $\{e\}$, with its zero-dimensional embedded Lie group structure, is compact, connected and abelian, hence is a torus. Taking it for $T_0$ proves existence for every compact $G$, including disconnected and zero-dimensional groups. The argument for arbitrary $T_0$ proves the containment assertion. No axiom of choice is needed by this proof beyond the retained, unused hypothesis [A1].