Metamath Proof Explorer


Syntax definition cltr

Description: Signed real ordering relation.

Ref Expression
Assertion cltr
class