Syntax Definition cins4 5755

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

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
cins4	class Ins4 A

See definition df-ins4 5756 for more information.