Syntax Definition cplc 4376

Description: Extend the definition of a class to include cardinal addition.

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
cplc	class (A +c B)

See definition df-addc 4379 for more information.