Syntax definition ctms

Description: Extend class notation with the function mapping a metric to the metric space it defines.

	Ref	Expression
Assertion	ctms	$$class\mathrm{toMetSp}$$