Metamath Proof Explorer


Syntax definition comnd

Description: Extend class notation with the class of all right ordered monoids.

Ref Expression
Assertion comnd class oMnd