Shorten using ssltd

set.mm

@@ -532858,23 +532858,22 @@ property of surreals and will be used (via surreal cuts) to prove many
     $( Union law for surreal set less than.  (Contributed by Scott Fenton,
        9-Dec-2021.) $)
     ssltun1 $p |- ( ( A <<s C /\ B <<s C ) -> ( A u. B ) <<s C ) $=
-      ( vx vy csslt wbr wa cvv wcel csur wss wral ssltex1 adantr ssltss1 adantl
-      cv ssltsep sylanbrc cun w3a unexg syl2an ssltex2 jca unssd ssltss2 ralunb
-      cslt 3jca brsslt ) ACFGZBCFGZHZABUAZIJZCIJZHUPKLZCKLZDRERUJGECMZDUPMZUBUP
-      CFGUOUQURUMAIJBIJUQUNACNBCNABIIUCUDUMURUNACUEOUFUOUSUTVBUOABKUMAKLUNACPOU
-      NBKLUMBCPQUGUNUTUMBCUHQUOVADAMZVADBMZVBUMVCUNDEACSOUNVDUMDEBCSQVADABUITUK
-      DEUPCULT $.
+      ( vx vy csslt wbr cvv wcel ssltex1 adantr adantl csur ssltss1 cv ssltsepc
+      wss wi 3exp com12 wa cun unexd ssltex2 unssd ssltss2 cslt elun jaoi sylbi
+      wo 3imp21 ssltd ) ACFGZBCFGZUAZDEABUBZCHHUPABHHUNAHIUOACJKUOBHIUNBCJLUCUN
+      CHIUOACUDKUPABMUNAMQUOACNKUOBMQUNBCNLUEUNCMQUOACUFKDOZUQIZUPEOZCIZURUTUGG
+      ZUSURAIZURBIZUKUPVAVBRZRZURABUHVCVFVDUPVCVEUNVCVERUOUNVCVAVBACURUTPSKTUPV
+      DVEUOVDVERUNUOVDVAVBBCURUTPSLTUIUJULUM $.
 
     $( Union law for surreal set less than.  (Contributed by Scott Fenton,
        9-Dec-2021.) $)
     ssltun2 $p |- ( ( A <<s B /\ A <<s C ) -> A <<s ( B u. C ) ) $=
-      ( vx vy csslt wbr wa cvv wcel csur wss wral adantr ssltex2 ssltss2 adantl
-      cv ssltsep sylanbrc cun w3a ssltex1 unexg syl2an jca ssltss1 unssd ralunb
-      cslt ralbii r19.26 bitri 3jca brsslt ) ABFGZACFGZHZAIJZBCUAZIJZHAKLZUTKLZ
-      DRERUJGZEUTMZDAMZUBAUTFGURUSVAUPUSUQABUCNUPBIJCIJVAUQABOACOBCIIUDUEUFURVB
-      VCVFUPVBUQABUGNURBCKUPBKLUQABPNUQCKLUPACPQUHURVDEBMZDAMZVDECMZDAMZVFUPVHU
-      QDEABSNUQVJUPDEACSQVFVGVIHZDAMVHVJHVEVKDAVDEBCUIUKVGVIDAULUMTUNDEAUTUOT
-      $.
+      ( vx vy csslt wbr cvv wcel adantr ssltex2 adantl csur ssltss2 cv ssltsepc
+      wss wi 3exp com3r wa cun ssltex1 unexd ssltss1 unssd cslt elun jaoi sylbi
+      wo 3imp231 ssltd ) ABFGZACFGZUAZDEABCUBZHHUNAHIUOABUCJUPBCHHUNBHIUOABKJUO
+      CHIUNACKLUDUNAMQUOABUEJUPBCMUNBMQUOABNJUOCMQUNACNLUFEOZUQIZUPDOZAIZUTURUG
+      GZUSURBIZURCIZUKUPVAVBRRZURBCUHVCVEVDUPVAVCVBUNVAVCVBRRUOUNVAVCVBABUTURPS
+      JTUPVAVDVBUOVAVDVBRRUNUOVAVDVBACUTURPSLTUIUJULUM $.
   $}
 
   ${