diff -r de9e5faf1f03 -r 46cc6708c3b3 Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 16:30:51 2010 +0100
@@ -535,6 +535,17 @@
 apply metis
 done
 
+lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
+  apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+  apply clarify
+  apply auto
+  apply (rule bexI)
+  apply assumption
+  apply (simp add: in_respects)
+  apply (simp add: in_respects)
+  apply auto
+  done
+
 section {* Various respects and preserve lemmas *}
 
 lemma quot_rel_rsp: