a complete set of S-polynomials each of which has $0$ as a $G$-remainder modulo $B$. Then $B$ is a $G$-Gröbner basis of the ideal generated by $GB$.

We will first prove this for [*ordinary*]{} Gröbner bases, and from that deduce the theorem for equivariant Gröbner bases. The proof for the ordinary case is identical to the proof in the case of finitely many variables. We include it for completeness, and also because we have no reference where the result is stated for infinitely many variables.

We may and will assume that all elements of $B$ are monic. Let $I$ denote the ideal generated by $B$. If ${\mathrm{lm}}(B)$ does not generate the ideal ${\mathrm{lm}}(I)$ in ${\mathrm{Mon}}$ then there exists a polynomial of the form $$f=\sum_{b \in B} f_{b} b$$ with only finitely many of the $f_{b}$ non-zero, for which ${\mathrm{lm}}(f)$ is not in the ideal generated by ${\mathrm{lm}}(B)$. We may choose the expression above such that first, the [*maximum*]{} $m$ of ${\mathrm{lm}}(f_{b}
b)$ over all $b$ for which $f_{b}$ is non-zero is [*minimal*]{} and second, the number of $b$ with ${\mathrm{lm}}(f_{b} b)=m$ is also minimal. The maximum is then attained for at least two values $b_0,b_1$ of $b$, because otherwise $m$ 