Tweak acycgrcycl

set.mm

@@ -501845,16 +501845,16 @@ it has no (non-trivial) cycles.  (Contributed by BTernaryTau,
   ${
     $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 = (/) ) ) $=
+       edges).  (Contributed by BTernaryTau, 12-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
-      $.
+      wlkv isacycgr1 ibi 19.21bbi adantr vtocl2d ex pm2.43d imp ) CFGZBACHIZJZB
+      KLZUTVBVCUTVBVBVCMZUTVBNDOZEOZVAJZVEKLZMZVDDEBAPPVBBPGZUTVBCPGZVJAPGZVBBA
+      CQIJVKVJVLRABCUAABCUKUBZUCSVBVLUTVBVKVJVLVMUDSVEBLZVIBVFVAJZVCMVFALZVDVNV
+      GVOVHVCVEBVFVAUEVEBKUFUGVPVOVBVCVFABVAUHUIUJUTVIVBUTVIDEUTVIETDTDCFEULUMU
+      NUOUPUQURUS $.
   $}
 
 $( (End of BTernaryTau's mathbox.) $)