Existence and Uniqueness of the Integer Part of a Real Number

Adopt the notation of the definition of the integers: $\mathbb{R}$ is the real numbers with the order $\le$ of its ordered field structure, $\mathbb{N}$ is the set of natural numbers, $\iota$ is the canonical map, and $\mathbb{Z}$ is the set of integers. For $s,t\in\mathbb{R}$ write $s<t$ to mean $s\le t$ and $s\ne t$.

For every $x\in\mathbb{R}$ there is exactly one $n\in\mathbb{Z}$ such that

This integer is written $\lfloor x\rfloor$ and called the integer part of $x$. It satisfies $x-1<\lfloor x\rfloor\le x$.