The justification of the use of Remove Redundant requires the following proposition.
Propostion 12.14 Let = (V,E) be a Gröbner graph, V be a finite set, and X be the set which is generated by RemoveRedundant when it is applied to G and . The ideal generated by equals the ideal generated by X.
Proof. For each , let be defined as in Lemma 12.13. Since , . To show that , it suffices to show that for . Let . Since , is not the empty set. Let be as in Lemma 12.13. is empty for each starting vertex w of . By Proposition 12.8, v lies in the ideal generated by the starting vertices of and so v lies in the ideal generated by X. This completes the proof of Proposition 12.14.
RemoveRedundant can be a very fast operation since it requires only the searching of graphs (which is fast in comparison to GBA which is what the previous two idealized operations used).