src/HOL/Analysis/Elementary_Normed_Spaces.thy

   show ?thesis
     by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
 qed
 
 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x \<le> b)"
-  apply (simp add: bounded_iff)
-  apply (subgoal_tac "\<And>x (y::real). 0 < 1 + \<bar>y\<bar> \<and> (x \<le> y \<longrightarrow> x \<le> 1 + \<bar>y\<bar>)")
-  apply metis
-  apply arith
-  done
+  unfolding bounded_iff 
+  by (meson less_imp_le not_le order_trans zero_less_one)
 
 lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
   apply (simp add: bounded_pos)
   apply (safe; rule_tac x="b+1" in exI; force)
   done