From d6fa64fa7f9a7cfcb51c3b297106f286e3aae91d Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Tue, 23 Jan 2024 00:31:51 +0100
Subject: [PATCH] comment correction

---
 set.mm | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/set.mm b/set.mm
index ad184d1a8..2da2dc4f6 100644
--- a/set.mm
+++ b/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 $.