Syntax definition cpstm

Description: Extend class notation with the metric induced by a pseudometric.

	Ref	Expression
Assertion	cpstm	$$class\mathrm{pstoMet}$$