diff -r 16375b493b64 -r 7d7627738e66 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue May 17 11:47:36 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue May 17 12:21:58 2011 +0200
@@ -658,6 +658,26 @@
   qed
 qed auto
 
+lemma borel_eq_atLeastLessThan:
+  "borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S")
+proof (intro algebra.equality antisym)
+  interpret sigma_algebra ?S
+    by (rule sigma_algebra_sigma) auto
+  show "sets borel \<subseteq> sets ?S"
+    unfolding borel_eq_lessThan
+  proof (intro sets_sigma_subset subsetI)
+    have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto
+    fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>"
+    then obtain x where "A = {..< x}" by auto
+    then have "A = (\<Union>i::nat. {-real i ..< x})"
+      by (auto simp: move_uminus real_arch_simple)
+    then show "A \<in> sets ?S"
+      by (auto simp: sets_sigma intro!: sigma_sets.intros)
+  qed simp
+  show "sets ?S \<subseteq> sets borel"
+    by (intro borel.sets_sigma_subset) auto
+qed simp_all
+
 lemma borel_eq_halfspace_le:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
    (is "_ = ?SIGMA")