Metamath Proof Explorer


Syntax definition cr

Description: Class of real numbers.

Ref Expression
Assertion cr
class RR