diff -r 8558e4a37b48 -r a0cfa9050fa8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:39:10 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:40:47 2015 +0200
@@ -1642,10 +1642,11 @@
   obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
   by atomize_elim (cases x, auto)
 
-lemma sets_eq_imp_space_eq:
-  "sets M = sets M' \<Longrightarrow> space M = space M'"
-  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
-  by blast
+lemma sets_le_imp_space_le: "sets A \<subseteq> sets B \<Longrightarrow> space A \<subseteq> space B"
+  by (auto dest: sets.sets_into_space)
+
+lemma sets_eq_imp_space_eq: "sets M = sets M' \<Longrightarrow> space M = space M'"
+  by (auto intro!: antisym sets_le_imp_space_le)
 
 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)