Metamath Proof Explorer

Syntax definition cr

Description: Class of real numbers.

Ref Expression
Assertion cr 
class RR