Syntax definition crrv

Description: Extend class notation with the class of real-valued random variables.

	Ref	Expression
Assertion	crrv	$$class{\mathrm{RndVar}}_{ℝ}$$