Metamath Proof Explorer - cltr

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition cltr 3793

Description: Signed real ordering relation.

**Assertion**
Ref	Expression
cltr

See definition df-ltr 3964 for more information.

Colors of variables: wff set class