diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 13 11:35:47 2014 +0200
@@ -1266,6 +1266,9 @@
 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)
 
+lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M"
+  using emeasure_notin_sets[of A M] by blast
+
 lemma measure_notin_sets: "A \<notin> sets M \<Longrightarrow> measure M A = 0"
   by (simp add: measure_def emeasure_notin_sets)