# HG changeset patch
# User paulson
# Date 826550352 -3600
# Node ID 630d881b51bdcfa77f7c8b1eab5bb6686c23b4f9
# Parent  02bbdc811ae7764378c5e2319fa22212311df0f3
New theorem: Inter_Un_subset

diff -r 02bbdc811ae7 -r 630d881b51bd src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Mar 11 14:18:06 1996 +0100
+++ b/src/ZF/equalities.ML	Mon Mar 11 14:19:12 1996 +0100
@@ -190,6 +190,10 @@
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
+goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
+by (fast_tac ZF_cs 1);
+qed "Inter_Un_subset";
+
 (* A good challenge: Inter is ill-behaved on the empty set *)
 goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
 by (fast_tac eq_cs 1);