diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -175,6 +175,12 @@
   shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
   by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
 
+lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a"
+  by auto
+
+lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
+  by auto
+
 subsection {*Two-sided intervals*}
 
 context ord