diff -r 6b5421bd0fc3 -r 496cfe488d72 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 05 21:03:31 2020 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Aug 06 13:07:23 2020 +0100
@@ -1280,6 +1280,28 @@
 lemma SUP_fold_sup: "finite A \<Longrightarrow> \<Squnion>(f ` A) = fold (sup \<circ> f) bot A"
   using sup_SUP_fold_sup [of A bot] by simp
 
+lemma finite_Inf_in:
+  assumes "finite A" "A\<noteq>{}" and inf: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> inf x y \<in> A"
+  shows "Inf A \<in> A"
+proof -
+  have "Inf B \<in> A" if "B \<le> A" "B\<noteq>{}" for B
+    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
+  by (induction B) (use inf in \<open>force+\<close>)
+  then show ?thesis
+    by (simp add: assms)
+qed
+
+lemma finite_Sup_in:
+  assumes "finite A" "A\<noteq>{}" and sup: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> sup x y \<in> A"
+  shows "Sup A \<in> A"
+proof -
+  have "Sup B \<in> A" if "B \<le> A" "B\<noteq>{}" for B
+    using finite_subset [OF \<open>B \<subseteq> A\<close> \<open>finite A\<close>] that
+  by (induction B) (use sup in \<open>force+\<close>)
+  then show ?thesis
+    by (simp add: assms)
+qed
+
 end