Syntax definition c-bnj14

Description: Extend class notation with the function giving: the class of all elements of A that are "smaller" than X according to R . (New usage is discouraged.)

	Ref	Expression
Assertion	c-bnj14	$$classpred\left(X,A,R\right)$$