src/HOL/Complete_Lattices.thy

--- a/src/HOL/Complete_Lattices.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1128,6 +1128,8 @@
 lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   by (fact Sup_subset_mono)
 
+lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
+  by blast
 
 subsubsection \<open>Unions of families\<close>