--- a/src/ZF/Constructible/AC_in_L.thy Thu Mar 22 10:10:02 2012 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Thu Mar 22 16:41:22 2012 +0000
@@ -4,7 +4,7 @@
header {* The Axiom of Choice Holds in L! *}
-theory AC_in_L imports Formula begin
+theory AC_in_L imports Formula Separation begin
subsection{*Extending a Wellordering over a List -- Lexicographic Power*}
@@ -452,6 +452,18 @@
apply (blast dest!: well_ord_L_r intro: well_ord_subset)
done
+interpretation L?: M_basic L by (rule M_basic_L)
+
+theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
+proof
+ fix x
+ assume "L(x)"
+ then obtain r where "well_ord(x,r)"
+ by (blast dest: L_implies_AC)
+ thus "\<exists>r. wellordered(L,x,r)"
+ by (blast intro: well_ord_imp_relativized)
+qed
+
text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know
that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''},
but this reasoning doesn't appear to work in Isabelle.*}