From 7c89ea6768ef601bce1f1dd8a094519da15da9f0 Mon Sep 17 00:00:00 2001
From: mazsa <peter@mazsa.com>
Date: Wed, 1 Jan 2025 17:58:35 +0100
Subject: [PATCH] WIP

---
 set.mm | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/set.mm b/set.mm
index eb535bb508..b5c8be840c 100644
--- a/set.mm
+++ b/set.mm
@@ -581984,9 +581984,10 @@ relation with an intersection with the same Cartesian product (see also
      (Contributed by Peter Mazsa, 18-Nov-2024.)
      (Proof modification is discouraged.) $)
   mopickr $p |- ( ( E* x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) ) $=
-    ( wmo wa wex wi exancom wn weu wo moeu2 bj-nexrt pm2.21 syl a1d eupickbi sp
-    wal syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUFBAECFZUEUGABCHUEBCFIZBCJ
-    ZKUHUGGZBCLUIUKUJUIUGUHUIBIUGBCMBANOPUJUHUGCSUGBACQUGCRTUAUBUCUD $.
+    ( wmo wa wex wi exancom wn weu wo moeu2 19.8a con3i pm2.21 syl a1d eupickbi
+    wal sp syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUGBAECFZUFUHABCHUFBCFZI
+    ZBCJZKUIUHGZBCLUKUMULUKUHUIUKBIUHBUJBCMNBAOPQULUIUHCSUHBACRUHCTUAUBUCUDUE
+    $.
 
   $( Sufficient condition for transitivity of conjunctions inside existential
      quantifiers.  (Contributed by Peter Mazsa, 2-Oct-2018.) $)