diff --git a/set.mm b/set.mm
index 1bfca43598..22916f272d 100644
--- a/set.mm
+++ b/set.mm
@@ -501842,6 +501842,21 @@ it has no (non-trivial) cycles.  (Contributed by BTernaryTau,
       JADUKUEUIUFUKUDUHUAUBUCBGNSOPAEDQT $.
   $}
 
+  ${
+    $d P f p $.  $d f F p $.  $d f G p $.
+    $( Any cycle in an acyclic graph is trivial (i.e. has one vertex and no
+       edges).  (Contributed by BTernaryTau, 11-Oct-2023.) $)
+    acycgrcycl $p |- ( G e. AcyclicGraph ->
+              ( F ( Cycles ` G ) P -> F = (/) ) ) $=
+      ( vf vp cacycgr wcel ccycls cfv wbr c0 wceq wi wa cv cvv cwlks w3a adantl
+      wal cycliswlk syl simp2d simp3d breq1 eqeq1 imbi12d breq2 imbi1d sylan9bb
+      wlkv isacycgr1 ibi 19.21bbi adantr vtocl2d ex pm2.43d ) CFGZBACHIZJZBKLZU
+      SVAVAVBMZUSVANDOZEOZUTJZVDKLZMZVCDEBAPPVABPGZUSVACPGZVIAPGZVABACQIJVJVIVK
+      RABCUAABCUKUBZUCSVAVKUSVAVJVIVKVLUDSVDBLZVHBVEUTJZVBMVEALZVCVMVFVNVGVBVDB
+      VEUTUEVDBKUFUGVOVNVAVBVEABUTUHUIUJUSVHVAUSVHDEUSVHETDTDCFEULUMUNUOUPUQUR
+      $.
+  $}
+
 $( (End of BTernaryTau's mathbox.) $)