--- a/src/ZF/Fixedpt.thy Tue Jun 18 17:58:21 2002 +0200
+++ b/src/ZF/Fixedpt.thy Tue Jun 18 18:45:07 2002 +0200
@@ -49,6 +49,18 @@
apply (rule Un_least, blast+)
done
+(*unused*)
+lemma bnd_mono_UN:
+ "[| bnd_mono(D,h); \<forall>i\<in>I. A(i) <= D |]
+ ==> (\<Union>i\<in>I. h(A(i))) <= h((\<Union>i\<in>I. A(i)))"
+apply (unfold bnd_mono_def)
+apply (rule UN_least)
+apply (elim conjE)
+apply (drule_tac x="A(i)" in spec)
+apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec)
+apply blast
+done
+
(*Useful??*)
lemma bnd_mono_Int:
"[| bnd_mono(D,h); A <= D; B <= D |] ==> h(A Int B) <= h(A) Int h(B)"