--- a/Quot/QuotScript.thy	Thu Dec 10 16:56:03 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 18:28:30 2009 +0100
@@ -31,6 +31,11 @@
   shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
 by (metis equivp_reflp_symp_transp transp_def)
 
+lemma equivpI:
+  assumes "reflp R" "symp R" "transp R"
+  shows "equivp R"
+using assms by (simp add: equivp_reflp_symp_transp)
+
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"