diff --git a/set.mm b/set.mm
index 9ad4aa6528..88a802e404 100644
--- a/set.mm
+++ b/set.mm
@@ -75869,8 +75869,7 @@ currently used conventions for such cases (see ~ cbvmpt2x , ~ ovmpt2x and
     ${
       $d x A $.
       $( A way of showing an ordinal function is one-to-one.  (Contributed by
-         NM, 9-Feb-1997.)  Avoid ~ ax-8 .  (Revised by Gino Giotto,
-         22-May-2023.) $)
+         NM, 9-Feb-1997.) $)
       tz7.48lem $p |- ( ( A C_ On /\ A. x e. A A. y e. x
                     -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) ) $=
         ( vw vz con0 cv cfv wceq wn wral wa weq wi wel wcel wal r2al cres simpl