GL's review remark

minor improvement of comment

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), 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 ).
+       proofs instead of its hard-coded, numeric 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