src/HOL/Orderings.thy

     and "\<And>y. P y \<Longrightarrow> x \<le> y"
     and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
   shows "Q (Least P)"
 unfolding Least_def by (rule theI2)
   (blast intro: assms antisym)+
+
+lemma Least_ex1:
+  assumes   "\<exists>!x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y)"
+  shows     Least1I: "P (Least P)" and Least1_le: "P z \<Longrightarrow> Least P \<le> z"
+  using     theI'[OF assms]
+  unfolding Least_def
+  by        auto
 
 text \<open>Greatest value operator\<close>
 
 definition Greatest :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREATEST " 10) where
 "Greatest P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<ge> y))"