[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] If $R:\mathbb{R} \times \mathbb{R} \to \mathrm{Prop}$ is an entire binary relation on the real numbers $\mathbb{R}$, then one can construct a sequence of real numbers $x:\mathbb{N} \to \mathbb{R}$ such that for all $n:\mathbb{N}$, $R(x(n), x(n+1))$. category: redirected to nlab