PR comments

set.mm

@@ -532656,20 +532656,20 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
     $( Relationship between surreal set less than and subset.  (Contributed by
        Scott Fenton, 9-Dec-2021.) $)
     sssslt1 $p |- ( ( A <<s B /\ C C_ A ) -> C <<s B ) $=
-      ( vx vy csslt wbr wss wa cvv wcel ssltex1 adantr simpr ssexd ssltex2 csur
-      ssltss1 sstrd cv ssltss2 cslt simp1l simp1r simp2 sseldd ssltsepc syl3anc
-      w3a simp3 ssltd ) ABFGZCAHZIZDECBJJUNCAJULAJKUMABLMULUMNZOULBJKUMABPMUNCA
-      QUOULAQHUMABRMSULBQHUMABUAMUNDTZCKZETZBKZUIZULUPAKUSUPURUBGULUMUQUSUCUTCA
-      UPULUMUQUSUDUNUQUSUEUFUNUQUSUJABUPURUGUHUK $.
+      ( vx vy csslt wbr wss wa cvv wcel csur cslt wral w3a ssltex1 adantr simpr
+      cv ssexd ssltex2 ssltss1 sstrd ssltss2 ssltsep ssralv mpan9 3jca brsslt
+      syl21anbrc ) ABFGZCAHZIZCJKBJKZCLHZBLHZDSESMGEBNZDCNZOCBFGUMCAJUKAJKULABP
+      QUKULRZTUKUNULABUAQUMUOUPURUMCALUSUKALHULABUBQUCUKUPULABUDQUKUQDANULURDEA
+      BUEUQDCAUFUGUHDECBUIUJ $.
 
     $( Relationship between surreal set less than and subset.  (Contributed by
        Scott Fenton, 9-Dec-2021.) $)
     sssslt2 $p |- ( ( A <<s B /\ C C_ B ) -> A <<s C ) $=
-      ( vx vy csslt wbr wss wa cvv wcel ssltex1 adantr ssltex2 simpr ssexd csur
-      ssltss1 ssltss2 cv sstrd cslt simp1l simp2 simp1r sseldd ssltsepc syl3anc
-      w3a simp3 ssltd ) ABFGZCBHZIZDEACJJULAJKUMABLMUNCBJULBJKUMABNMULUMOZPULAQ
-      HUMABRMUNCBQUOULBQHUMABSMUAUNDTZAKZETZCKZUIZULUQURBKUPURUBGULUMUQUSUCUNUQ
-      USUDUTCBURULUMUQUSUEUNUQUSUJUFABUPURUGUHUK $.
+      ( vx vy csslt wbr wss wa cvv wcel csur cv cslt w3a ssltex1 adantr ssltex2
+      wral simpr ssexd ssltss1 ssltss2 sstrd ssltsep ssralv ralimdv 3jca brsslt
+      mpan9 syl21anbrc ) ABFGZCBHZIZAJKZCJKALHZCLHZDMEMNGZECSZDASZOACFGULUOUMAB
+      PQUNCBJULBJKUMABRQULUMTZUAUNUPUQUTULUPUMABUBQUNCBLVAULBLHUMABUCQUDULUREBS
+      ZDASUMUTDEABUEUMVBUSDAURECBUFUGUJUHDEACUIUK $.
   $}
 
   ${
@@ -533156,7 +533156,7 @@ property of surreals and will be used (via surreal cuts) to prove many
 
   ${
     $d A a b c $.  $d B a b c x $.  $d C a b c x y $.
-    $( If ` B ` is conitial with ` C ` and ` A ` precedes ` C ` , then ` A `
+    $( If ` B ` is coinitial with ` C ` and ` A ` precedes ` C ` , then ` A `
        precedes ` B ` .  (Contributed by Scott Fenton, 24-Sep-2024.) $)
     coinitsslt $p |- ( ( B e. ~P No /\
      A. x e. B E. y e. C y <s x /\ A <<s C ) -> A <<s B ) $=
@@ -533901,7 +533901,7 @@ property of surreals and will be used (via surreal cuts) to prove many
 
   ${
     $d X x y $.  $d Y x y $.
-    $( If ` A ` is less than ` B ` , then either ` ( _L `` Y ) ` or
+    $( If ` X ` is less than ` Y ` , then either ` ( _L `` Y ) ` or
        ` ( _R `` X ) ` is non-empty.  (Contributed by Scott Fenton,
        10-Dec-2024.) $)
     sltn0 $p |- ( ( X e. No /\ Y e. No /\ X <s Y ) ->