diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md
index 474843090b..12006b0e50 100644
--- a/src/real-numbers/dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/dedekind-real-numbers.lagda.md
@@ -195,7 +195,7 @@ pr2 (ℝ-Set l) = is-set-ℝ l
 
 ## Properties of lower/upper Dedekind cuts
 
-Lower and upper Dedekind cuts are stable under `le-ℚ` and `leq-ℚ`
+### Lower and upper Dedekind cuts are closed under the standard ordering on the rationals
 
 ```agda
 module _