Metamath Proof Explorer


Syntax definition cltq

Description: Positive fraction ordering relation.

Ref Expression
Assertion cltq class <Q