Syntax definition coch

Description: Extend class notation with subspace orthocomplement for DVecH vector space.

	Ref	Expression
Assertion	coch	$$class\mathrm{ocH}$$