Syntax Definition cclos1 5872

Description: Extend the definition of a class to include the closure operation.

Hypotheses

Ref	Expression
cA	class A
cR	class R

Assertion

Ref	Expression
cclos1	class Clos1 (A, R)

See definition df-clos1 5873 for more information.