Metamath Proof Explorer


Syntax definition cxrs

Description: Extend class notation with the extended real number structure.

Ref Expression
Assertion cxrs
class RR*s