add comment on trcl revision

metamath · Dec 11, 2024 · 81b20d9 · 81b20d9
1 parent d525d10
commit 81b20d9
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/set.mm b/set.mm
@@ -101777,8 +101777,8 @@ a Cantor normal form (and injectivity, together with coherence
   ${
     $d R w z $.  $d A w z $.
     $( Lemma for general well-founded recursion.  Establish a subset
-       relationship.  (Contributed by Scott Fenton, 11-Sep-2023.)  (Revised by
-       Scott Fenton, 1-Dec-2024.) $)
+       relationship.  (Contributed by Scott Fenton, 11-Sep-2023.)  Revised
+       notion of transitive closure.  (Revised by Scott Fenton, 1-Dec-2024.) $)
     frrlem16 $p |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) ->
        A. w e. Pred ( t++ ( R |` A ) , A , z )
        Pred ( R , A , w ) C_ Pred ( t++ ( R |` A ) , A , z ) ) $=