diff -r 0d6d37d0589d -r e3a963e6418b QuotScript.thy
--- a/QuotScript.thy	Fri Oct 16 16:51:01 2009 +0200
+++ b/QuotScript.thy	Fri Oct 16 17:05:52 2009 +0200
@@ -307,8 +307,14 @@
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using a
-by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+  and   "R (Rep (Abs x1)) x2"
+proof -
+  show "R x1 (Rep (Abs x2))" 
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+next
+  show "R (Rep (Abs x1)) x2"
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
+qed
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)