# HG changeset patch
# User lcp
# Date 776967176 -7200
# Node ID 972119df615e16127a4920d89652a6ce75ca6563
# Parent  e1de521e012af44133695c46e7972e7482ed86bd
ZF/CardinalArith/InfCard_Un: new

diff -r e1de521e012a -r 972119df615e src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Mon Aug 15 18:11:00 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Mon Aug 15 18:12:56 1994 +0200
@@ -347,6 +347,12 @@
 by (etac conjunct1 1);
 val InfCard_is_Card = result();
 
+goalw CardinalArith.thy [InfCard_def]
+    "!!K L. [| InfCard(K);  Card(L) |] ==> InfCard(K Un L)";
+by (asm_simp_tac (ZF_ss addsimps [Card_Un, Un_upper1_le RSN (2,le_trans), 
+				  Card_is_Ord]) 1);
+val InfCard_Un = result();
+
 (*Kunen's Lemma 10.11*)
 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)";
 by (etac conjE 1);