Theorem 12.5. $RG$ has quantifier elimination.