add the definition of transitive closure of a class

set.mm

@@ -444311,6 +444311,11 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
     "<IMG SRC='_pred.gif' WIDTH=30 HEIGHT=19 ALT=' Pred' TITLE='Pred'>";
   althtmldef "Pred" as "Pred";
   latexdef "Pred" as "\mathrm{Pred}";
+htmldef "t++" as "<IMG SRC='t.gif' WIDTH=7 HEIGHT=19 ALT=' t' TITLE='t'>" +
+    "<IMG SRC='plus.gif' WIDTH=13 HEIGHT=19 ALT='+' TITLE='+'>" +
+    "<IMG SRC='plus.gif' WIDTH=13 HEIGHT=19 ALT='+' TITLE='+'>";
+  althtmldef "t++" as "t++";
+  latexdef "t++" as "\mathrm{t}++";
 htmldef "TrPred" as
     "<IMG SRC='_trpred.gif' WIDTH=44 HEIGHT=19 ALT=' TrPred' TITLE='TrPred'>";
   althtmldef "TrPred" as "TrPred";
@@ -527407,6 +527412,31 @@ Set induction (or epsilon induction)
       VNAVMVACVBVGUJABVGUEUFUGUHUIVEVKUKULABVGIVPRUMUNDVFUOUPUQABIURUS $.
   $}
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Transitive closure of a class
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $( Declare new constant $)
+  $c t++ $.
+
+  $( Declare the syntax for the transitive closure of a class.  See
+     ~ df-ttcl . $)
+  cttcl $a class t++ R $.
+
+  ${
+     $d R f n m x y $.
+     $( Define the transitive closure of a class.  This is the smallest
+        relationship containing ` R ` and having the transitive property.
+	Definition from [Levy] p. 59, who denotes it as ` R * ` and calls
+	it the "ancestral" of ` R ` .  (Contributed by Scott Fenton,
+	17-Oct-2024.) $)
+     df-ttrcl $a |- t++ R = { <. x , y >. | E. n e. ( _om \ 2o )
+     E. f ( f Fn n /\ ( ( f ` (/) ) = x /\ ( f ` U. n ) = y ) /\
+     A. m e. U. n ( f ` m ) R ( f ` suc m ) ) } $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=