diff -r 1144d7ec892a -r d1a937cbf858 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Tue May 13 11:35:47 2014 +0200
@@ -467,6 +467,12 @@
   "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
 by (auto simp: set_eq_iff intro: top_le le_bot)
 
+lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
+  by (auto simp: set_eq_iff not_less le_bot)
+
+lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+  by (simp add: Iio_eq_empty_iff bot_nat_def)
+
 
 subsection {* Infinite intervals *}