diff --git a/set.mm b/set.mm
index 7013d3058f..52ff0142a2 100644
--- a/set.mm
+++ b/set.mm
@@ -487083,8 +487083,8 @@ its graph has a given second element (that is, function value).
     nn0difffzod.1 $e |- ( ph -> N e. ZZ ) $.
     nn0difffzod.2 $e |- ( ph -> M e. ( NN0 \ ( 0 ..^ N ) ) ) $.
     $( Membership in the nonnegative integers, except a half-open range
-       starting from zero, implies a strict inequality.  (Contributed by
-       Thierry Arnoux, 20-Feb-2025.) $)
+       starting from zero, implies inequality.  (Contributed by Thierry Arnoux,
+       20-Feb-2025.) $)
     nn0difffzod $p |- ( ph -> -. M < N ) $=
       ( cc0 cfzo co wcel wn cn0 cz clt wbr eldifbd eldifad wa wi w3a elfzo0z
       biimpri 3expa con3i imnan sylibr imp syl12anc ) ABFCGHZIZJZBKIZCLIZBCMNZJ