Comment

metamath · Feb 20, 2025 · 99fc25b · 99fc25b
1 parent dfbc151
commit 99fc25b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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