src/HOL/Analysis/Path_Connected.thy
changeset 68120 2f161c6910f7
parent 68096 e58c9ac761cb
child 68296 69d680e94961
     1.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -6981,7 +6981,7 @@
     1.4      shows "S = {}"
     1.5  proof -
     1.6    obtain a b where "S \<subseteq> box a b"
     1.7 -    by (meson assms bounded_subset_open_interval)
     1.8 +    by (meson assms bounded_subset_box_symmetric)
     1.9    then have "a \<notin> S" "b \<notin> S"
    1.10      by auto
    1.11    then have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> - S"