--- a/QuotScript.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/QuotScript.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -501,21 +501,25 @@
 *)
 lemma FORALL_PRS:
   assumes a: "QUOTIENT R absf repf"
-  shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
-  sorry
+  shows "All f = Ball (Respects R) ((absf ---> id) f)"
+  using a
+  unfolding QUOTIENT_def
+  by (metis IN_RESPECTS fun_map.simps id_apply)
 
 lemma EXISTS_PRS:
   assumes a: "QUOTIENT R absf repf"
-  shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
-  sorry
+  shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
+  using a
+  unfolding QUOTIENT_def
+  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
+   
+lemma ho_all_prs: 
+  shows "op = ===> op = ===> op = All All"
+  by auto
 
-lemma ho_all_prs: "op = ===> op = ===> op = All All"
-  apply (auto)
-  done
-
-lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex"
-  apply (auto)
-  done
+lemma ho_ex_prs: 
+  shows "op = ===> op = ===> op = Ex Ex"
+  by auto
 
 end