[267]Supponiamo che ≤ sia una relazione di ordine (possibilmente parziale) su ℕ soddisfacente [26H]↺↻ allora ≤ è unico.
[270]↺↻