--- a/Closures2.thy	Fri Sep 02 14:29:54 2011 +0000
+++ b/Closures2.thy	Sun Sep 04 00:21:41 2011 +0000
@@ -245,9 +245,9 @@
   from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast
   have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)
   moreover
-  have "f i \<in> A" sorry
+  have "f i \<in> A" using c by auto
   moreover
-  have "f j \<in> A" sorry
+  have "f j \<in> A" using c by auto
   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   with e show "False" by simp
 qed