diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index b8c048ff61..2ef3432f82 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -46,7 +46,7 @@ the [image](foundation.images.md) of this embedding ## Definitions -### Strict inequality on rational gives Dedekind cuts +### Strict inequality on rationals gives Dedekind cuts ```agda is-dedekind-cut-le-ℚ :