Metamath Proof Explorer - cltp

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cltp 3783

Description: Positive real ordering relation.

**Assertion**
Ref	Expression
cltp	class <_P

See definition df-ltp 3884 for more information.

Colors of variables: wff set class