Syntax Definition csup 4573

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 4574 for more information.

Copyright terms: Public domain