src/HOL/SetInterval.thy

--- a/src/HOL/SetInterval.thy	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Aug 26 16:13:19 2009 +0200
@@ -242,6 +242,14 @@
 
 end
 
+lemma (in linorder) atLeastLessThan_subset_iff:
+  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
+apply (auto simp:subset_eq Ball_def)
+apply(frule_tac x=a in spec)
+apply(erule_tac x=d in allE)
+apply (simp add: less_imp_le)
+done
+
 subsection {* Intervals of natural numbers *}
 
 subsubsection {* The Constant @{term lessThan} *}