src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Relation.thy	Fri Jan 13 16:19:56 2023 +0000
@@ -1247,6 +1247,9 @@
 definition Field :: "'a rel \<Rightarrow> 'a set"
   where "Field r = Domain r \<union> Range r"
 
+lemma Field_iff: "x \<in> Field r \<longleftrightarrow> (\<exists>y. (x,y) \<in> r \<or> (y,x) \<in> r)"
+  by (auto simp: Field_def)
+
 lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
   unfolding Field_def by blast