Syntax definition chcmp

Description: Extend class notation with the Hausdorff uniform completion relation.

	Ref	Expression
Assertion	chcmp	$$class\mathrm{HCmp}$$