# HG changeset patch
# User paulson
# Date 833795035 -7200
# Node ID 036a7f3016233468ac2363150092cfd8a0d13cd2
# Parent  173ce86b4c22fc31de778f98a4aaff6cdabc1ba8
Added a new theorem, UN_Int_subset

diff -r 173ce86b4c22 -r 036a7f301623 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Jun 03 11:41:26 1996 +0200
+++ b/src/ZF/equalities.ML	Mon Jun 03 11:43:55 1996 +0200
@@ -270,6 +270,10 @@
 by (fast_tac eq_cs 1);
 qed "INT_Int_distrib";
 
+goal ZF.thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
+by (fast_tac ZF_cs 1);
+qed "UN_Int_subset";
+
 (** Devlin, page 12, exercise 5: Complements **)
 
 goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";