--- a/src/HOL/BNF_Wellorder_Relation.thy Sat Jun 25 09:50:40 2022 +0000
+++ b/src/HOL/BNF_Wellorder_Relation.thy Mon Jun 27 15:54:18 2022 +0200
@@ -190,6 +190,9 @@
using assms ANTISYM unfolding antisym_def using TOTALS
unfolding max2_def by auto
+lemma in_notinI:
+assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
+shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>