Declaration le_decl

Declaration. le_decl
x ≤ y ↔ _

Declares less than or equal for real numbers to be a primitive predicate symbol. It is characterized by axioms rather than given by a definition.