Metamath Proof Explorer


Syntax definition cltp

Description: Positive real ordering relation.

Ref Expression
Assertion cltp class <P