comment correction

set.mm

@@ -26636,11 +26636,11 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d y A $.  $d x z $.  $d x y $.
     hblem.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
-       (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.)  Add disjoint variable condition to avoid ~ ax-13 .  See
-       ~ hblemg for a less restrictive version requiring more axioms.  (Revised
-       by Gino Giotto, 20-Jan-2024.) $)
+    $( Change the free variable of a hypothesis builder.  (Contributed by NM,
+       21-Jun-1993.)  (Revised by Andrew Salmon, 11-Jul-2011.)  Add disjoint
+       variable condition to avoid ~ ax-13 .  See ~ hblemg for a less
+       restrictive version requiring more axioms.  (Revised by Gino Giotto,
+       20-Jan-2024.) $)
     hblem $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsbw clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAE
       JBCDKZOPAQLM $.
@@ -26649,9 +26649,8 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d y A $.  $d x z $.
     hblemg.1 $e |- ( y e. A -> A. x y e. A ) $.
-    $( Change the free variable of a hypothesis builder.  Lemma for ~ nfcrii .
-       (Contributed by NM, 21-Jun-1993.)  (Revised by Andrew Salmon,
-       11-Jul-2011.) $)
+    $( Change the free variable of a hypothesis builder.  (Contributed by NM,
+       21-Jun-1993.)  (Revised by Andrew Salmon, 11-Jul-2011.) $)
     hblemg $p |- ( z e. A -> A. x z e. A ) $=
       ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ
       BCDKZOPAQLM $.