\begin{definition}[Definition:Real Number/Axioms]
The properties of the field of real numbers $\struct {\R, +, \times, \le}$ are as follows:
{{begin-axiom}}
{{axiom | n = \R \text A 0
        | lc= Closure under addition
        | q = \forall x, y \in \R
        | m = x + y \in \R
}}
{{axiom | n = \R \text A 1
        | lc= Associativity of addition
        | q = \forall x, y, z \in \R
        | m = \paren {x + y} + z = x + \paren {y + z}
}}
{{axiom | n = \R \text A 2
        | lc= Commutativity of addition
        | q = \forall x, y \in \R
        | m = x + y = y + x
}}
{{axiom | n = \R \text A 3
        | lc= Identity element for addition
        | q = \exists 0 \in \R: \forall x \in \R
        | m = x + 0 = x = 0 + x
}}
{{axiom | n = \R \text A 4
        | lc= Inverse elements for addition
        | q = \forall x: \exists \paren {-x} \in \R
        | m = x + \paren {-x} = 0 = \paren {-x} + x
}}
{{axiom | n = \R \text M 0
        | lc= Closure under multiplication
        | q = \forall x, y \in \R
        | m = x \times y \in \R
}}
{{axiom | n = \R \text M 1
        | lc= Associativity of multiplication
        | q = \forall x, y, z \in \R
        | m = \paren {x \times y} \times z = x \times \paren {y \times z}
}}
{{axiom | n = \R \text M 2
        | lc= Commutativity of multiplication
        | q = \forall x, y \in \R
        | m = x \times y = y \times x
}}
{{axiom | n = \R \text M 3
        | lc= Identity element for multiplication
        | q = \exists 1 \in \R, 1 \ne 0: \forall x \in \R
        | m = x \times 1 = x = 1 \times x
}}
{{axiom | n = \R \text M 4
        | lc= Inverse elements for multiplication
        | q = \forall x \in \R_{\ne 0}: \exists \frac 1 x \in \R_{\ne 0}
        | m = x \times \frac 1 x = 1 = \frac 1 x \times x
}}
{{axiom | n = \R \text D
        | lc= Multiplication is distributive over addition
        | q = \forall x, y, z \in \R
        | m = x \times \paren {y + z} = \paren {x \times y} + \paren {x \times z}
}}
{{axiom | n = \R \text O 1
        | lc= Usual ordering is compatible with addition
        | q = \forall x, y, z \in \R
        | m = x > y \implies x + z > y + z
}}
{{axiom | n = \R \text O 2
        | lc= Usual ordering is compatible with multiplication
        | q = \forall x, y, z \in \R
        | m = x > y, z > 0 \implies x \times z > y \times z
}}
{{axiom | n = \R \text O 3
        | lc= $\struct {\R, +, \times, \le}$ is Dedekind complete
        | q = 
        | m = 
}}
{{end-axiom}}
These are called the '''real number axioms'''.
\end{definition}