Fibre dimension and orbit dimension add to the dimension of the group

By [F1] the group $G$ is an irreducible classical variety, the orbit $O_x$ is a smooth locally closed $G$-stable subscheme, and ${\varrho }_x:G\to O_x$ is faithfully flat, hence surjective; as a continuous image of the irreducible space $G$ the space $O_x$ is irreducible, so ${\varrho }_x$ is a dominant morphism of irreducible classical varieties.

Applying [F3] to ${\varrho }_x:G\to O_x$ gives a nonempty open $U\subseteq O_x$ such that every fibre of ${\varrho }_x$ over a closed point of $U$ is nonempty and has pure dimension $\dim G-\dim O_x$; every closed point of $U$ is a closed point of $O_x$, hence lies in $O_x(k)$.

Every closed $k$-point $y$ of $O_x$ lifts to a $k$-point of $G$: the fibre over $y$ is nonempty of finite type over $k$ and hence has a $k$-point by [F5]. Consequently $y=g_{0}x$ for some $g_0\in G(k)$, and by [F2] the fibre is the translate $g_0{G}_x$, whose underlying space is homeomorphic to that of $G_x$; so every closed-point fibre has underlying topological dimension $\dim G_x$, equivalently the dimension of its reduction. This is assertion (a).

By steps 2.1 and 2.2 the generic closed-point fibres have dimension both $\dim G-\dim O_x$ and $\dim G_x$; comparing these two descriptions gives $\dim G=\dim G_x+\dim O_x$, which is assertion (b).

Let $Z=\overline{O_x}$ be the orbit closure, an irreducible closed subvariety of $X$; since $O_x$ is dense and locally closed in $Z$, it is open in $Z$, and the boundary $B=Z\setminus O_x$ is a proper closed $G$-stable subset. Being a proper closed subset of the irreducible $Z$, $B$ has dimension strictly smaller than $\dim Z=\dim O_x$ by [F4]; every orbit contained in $B$ has closure contained in $B$, hence dimension at most $\dim B$, by the same dimension comparison applied to that orbit.

This proves (c): the closure $\overline{O_x}=O_x\cup B$ is the union of $O_x$ and of orbits of strictly smaller dimension. If an orbit $O$ has minimal dimension among all orbits in $X$, then its boundary orbit closures would be orbits of strictly smaller dimension, contradicting minimality; hence $O$ is closed. Finally, starting from $\overline{O_x}$, replace the current orbit by an orbit in its boundary whenever the boundary is nonempty: the dimensions strictly decrease in the nonnegative integers, so after finitely many steps one reaches an orbit whose boundary is empty, that is, a closed orbit contained in $\overline{O_x}$; such an orbit exists because every nonempty closed subset contains a closed point by [F5], hence an orbit.