Syntax Definition csup 6947

Description: Extend class notation to include supremum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.

Hypotheses

Ref	Expression
cA	class A
cB	class B
cR	class R

Assertion

Ref	Expression
csup	class sup ( A , B , R )

See definition df-sup 6949 for more information.