src/HOL/Complete_Partial_Order.thy

--- a/src/HOL/Complete_Partial_Order.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -53,6 +53,9 @@
 lemma chain_empty: "chain ord {}"
 by(simp add: chain_def)
 
+lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
+by(auto simp add: chain_def)
+
 subsection {* Chain-complete partial orders *}
 
 text {*