Metamath Proof Explorer


Syntax definition corng

Description: Extend class notation with the class of all ordered rings.

Ref Expression
Assertion corng class oRing