Syntax definition ctx

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

	Ref	Expression
Assertion	ctx	class tX