diff --git a/set.mm b/set.mm
index 44f6186079..d0ba28fe82 100644
--- a/set.mm
+++ b/set.mm
@@ -200624,18 +200624,18 @@ function value at a particular slot (with index ` A ` ).
        typically used to refer to the number of a slot when defining structures
        without having to expose the detail of what that number is (for
        instance, we use the expression ` ( Base `` ndx ) ` in theorems and
-       proofs instead of its value 1).  Therefore, the usage of the specific
-       definition slot extractors like ` Base = Slot 1 ` (see ~ df-base ) is
-       discouraged.  Actually, these definitions are used in two basic theorems
-       named *id (theorems of the form ` C = Slot ( C `` ndx ) ` ) and *ndx
-       (theorems of the form ` ( C `` ndx ) = N ` ) only (see, for example,
-       ~ baseid and ~ basendx ), except additionally in the discouraged theorem
-       ~ baseval to demonstrate the representations of the value of the base
-       set extractor.  The *id theorems are implementation independent
-       equivalents of the definitions by the means of ~ ndxid , but the *ndx
-       theorems still depend on the hard-coded values of the indices.
-       Therefore, the usage of these *ndx theorems is also discouraged (for
-       more details see comment on ~ basendx ).
+       proofs instead of its value 1), and discourage using the specific
+       definition of slot extractors like ` Base = Slot 1 ` (see ~ df-base ).
+       Actually, these definitions are used in two basic theorems named *id
+       (theorems of the form ` C = Slot ( C `` ndx ) ` ) and *ndx (theorems of
+       the form ` ( C `` ndx ) = N ` ) only (see, for example, ~ baseid and
+       ~ basendx ), except additionally in the discouraged theorem ~ baseval to
+       demonstrate the representations of the value of the base set extractor.
+       The *id theorems are implementation independent equivalents of the
+       definitions by the means of ~ ndxid , but the *ndx theorems still depend
+       on the hard-coded values of the indices.  Therefore, the usage of these
+       *ndx theorems is also discouraged (for more details see the section
+       header comment ~ mmtheorems.html#cnx ).
 
        Example:  The group operation is the second component, i.e., the
        component in the second slot, of a group-like structure
@@ -200788,20 +200788,21 @@ when showing that a set of indices are disjoint (for example in proofs such
 
   As for the inequalities, it is recommended to provide them explicitly as
   theorems like ~ basendxnplusgndx , whenever they are required.  Since these
-  theorems are proved by discouraged theorems, they should be placed near the
+  theorems use discouraged slot theorems, they should be placed near the
   definition of a slot (within the same subsection), so that the range of
   usages of discouraged theorems is tightly limited.  Although there could be
-  quadradically many of them in the total number of indices, there actually
-  much less already available (and not much more are expected).
+  quadradically many of them in the total number of indices, much less are
+  actually available (and not much more are expected).
 
   As for the ordering, there are some theorems like ~ basendxltplusgndx
   providing the less-than relationship between two indices.  These theorems are
   also proved by discouraged theorems, so they should be placed near the
-  definition of a slot (within the same subsection), too.  Since such theorems
-  are rarely used (in structure building theorems *str like ~ rngstr ), it is
-  not recommended to provide explicit theorems for all of them, but to use the
-  (discouraged) *ndx theorems as in ~ lmodstr .  Therefore, such *str are
-  depending in general on the hard-coded values of the indices.
+  definition of a slot (within the same subsection), too.  However, since such
+  theorems are rarely used (in structure building theorems *str like
+  ~ rngstr ), it is not recommended to provide explicit theorems for all of
+  them, but to use the (discouraged) *ndx theorems as in ~ lmodstr .
+  Therefore, *str theorems generally depend on the hard-coded values of the
+  indices.
 
 $)
 
@@ -261913,7 +261914,7 @@ such that every prime ideal contains a prime element (this is a
     UUAWTXAXBWKACXCXFAXKXDTXEXGT $.
 
   $( The field of complex numbers is a function.  Alternate proof of ~ cnfldfun
-     not requireing that the index set of the components is ordered, but using
+     not requiring that the index set of the components is ordered, but using
      quadratically many inequalities for the indices.  (Contributed by AV,
      14-Nov-2021.)  (Proof shortened by AV, 11-Nov-2024.)
      (Proof modification is discouraged.)  (New usage is discouraged.) $)