src/ZF/func.thy

--- a/src/ZF/func.thy	Wed Jul 09 12:41:47 2003 +0200
+++ b/src/ZF/func.thy	Thu Jul 10 17:14:41 2003 +0200
@@ -509,7 +509,7 @@
 by blast  
 
 (*Intersection is ANTI-monotonic.  There are TWO premises! *)
-lemma Inter_anti_mono: "[| A<=B;  a:A |] ==> Inter(B) <= Inter(A)"
+lemma Inter_anti_mono: "[| A<=B;  A\<noteq>0 |] ==> Inter(B) <= Inter(A)"
 by blast
 
 lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"