Metamath Proof Explorer


Syntax definition cltb

Description: Ordering on terms of a multivariate polynomial.

Ref Expression
Assertion cltb class < bag