Syntax Definition ctfin 4436

Description: Extend class notation to include the finite T operation.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
ctfin	class Tfin A

See definition df-tfin 4444 for more information.