Syntax definition cldgis

Description: The leading ideal sequence used in the Hilbert Basis Theorem.

	Ref	Expression
Assertion	cldgis	$$class\mathrm{ldgIdlSeq}$$