Share distinct variable conditions

set.mm

@@ -501800,16 +501800,13 @@ have become an indirect lemma of the theorem in question (i.e. a lemma
   cacycgr $a class AcyclicGraph $.
 
   ${
-    $d g f p $.
+    $d f g p $.
     $( Define the class of all acyclic graphs.  A graph is called _acyclic_ if
        it has no (non-trivial) cycles.  (Contributed by BTernaryTau,
        11-Oct-2023.) $)
     df-acycgr $a |- AcyclicGraph =
               { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) } $.
-  $}
 
-  ${
-    $d f g p $.
     $( An alternate definition of the class of all acyclic graphs that requires
        all cycles to be trivial.  (Contributed by BTernaryTau, 11-Oct-2023.) $)
     dfacycgr1 $p |- AcyclicGraph =
@@ -501829,10 +501826,7 @@ it has no (non-trivial) cycles.  (Contributed by BTernaryTau,
       ( vg cv ccycls cfv wbr c0 wne wa wex wn cacycgr wceq fveq2 anbi1d 2exbidv
       breqd notbid df-acycgr elab2g ) AFZDFZEFZGHZIZUDJKZLZDMAMZNUDUEBGHZIZUILZ
       DMAMZNEBOCUFBPZUKUOUPUJUNADUPUHUMUIUPUGULUDUEUFBGQTRSUAAEDUBUC $.
-  $}
 
-  ${
-    $d f g G p $.
     $( The property of being an acyclic graph.  (Contributed by BTernaryTau,
        11-Oct-2023.) $)
     isacycgr1 $p |- ( G e. W -> ( G e. AcyclicGraph <->