Syntax definition ctx

Description: Extend class notation with the binary topological product operation.

	Ref	Expression
Assertion	ctx	$$class{\times }_t$$