Metamath Proof Explorer


Syntax definition cltpq

Description: Positive pre-fraction ordering relation.

Ref Expression
Assertion cltpq class <pQ