diff -r ab83ba2cd5d1 -r 251df82c0088 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 01 19:42:09 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 01 20:09:41 2010 +0100
@@ -397,6 +397,12 @@
     by (auto intro: sigma_sets.Empty sigma_sets_top)
 qed
 
+lemma (in sigma_algebra) sets_sigma_subset:
+  assumes "space N = space M"
+  assumes "sets N \<subseteq> sets M"
+  shows "sets (sigma N) \<subseteq> sets M"
+  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
+
 section {* Measurable functions *}
 
 definition
@@ -1149,7 +1155,6 @@
 
 section {* Dynkin systems *}
 
-
 locale dynkin_system =
   fixes M :: "'a algebra"
   assumes space_closed: "sets M \<subseteq> Pow (space M)"