Metamath Proof Explorer


Syntax definition crrext

Description: Extend class notation with the class of extension fields of RR .

Ref Expression
Assertion crrext class ℝExt