I recently came across the following Theorem in Gibson (Singular points of smooth mappings, 1979). Since I haven't seen this result somewhere else and this reference is not so widespread, I was wondering if it is correct, known or trivial?
Theorem B4 in Gibson79: Let $\phi: G \times M \to M$ be a smooth action of a Lie group $G$ on a smooth manifold $M$. Suppose that the action is semi-algebraic (i.e., the graph of $\phi$ is a semi-algebraic set). Then all the orbits are smooth submanifolds of $M$.
(Smooth means $C^\infty$; smooth submanifold means a differential manifold that is embedded.)
The proof goes as follows. The orbit at $x \in M$ is semi-algebraic by Tarski-Seidenberg. Every non-void semi-algebraic has at least a one neighbourhood where it is a submanifold in $M$. Since orbits are homogeneous by the action of $G$, this neigbourhood extends to the whole orbit.