Metamath Proof Explorer


Syntax definition cltrr

Description: 'Less than' predicate (defined over real subset of complex numbers).

Ref Expression
Assertion cltrr class <