--- a/src/HOL/Set_Interval.thy Mon Mar 04 09:57:54 2013 +0100
+++ b/src/HOL/Set_Interval.thy Wed Feb 20 12:04:42 2013 +0100
@@ -330,6 +330,20 @@
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
using atLeastLessThan_inj assms by auto
+context complete_lattice
+begin
+
+lemma atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+ by (auto simp: set_eq_iff intro: le_bot)
+
+lemma atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+ by (auto simp: set_eq_iff intro: top_le)
+
+lemma atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
+ by (auto simp: set_eq_iff intro: top_le le_bot)
+
+end
+
subsubsection {* Intersection *}
context linorder