src/ZF/AC/AC17_AC1.ML

 \       ==> EX r. well_ord(x,r)";
 by (rtac exI 1);
 by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj,
                 Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1);
 by (assume_tac 1);
-val UN_eq_imp_well_ord = result();
+qed "UN_eq_imp_well_ord";
 
 (* *********************************************************************** *)
 (* theorems closer to the proof                                            *)
 (* *********************************************************************** *)
 

 by (res_inst_tac [("x","Union(A)")] exI 1);
 by (rtac ballI 1);
 by (etac swap 1);
 by (rtac impI 1);
 by (fast_tac (!claset addSIs [restrict_type]) 1);
-val not_AC1_imp_ex = result();
+qed "not_AC1_imp_ex";
 
 goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u;  \
 \       EX f: Pow(x)-{0}->x. \
 \       x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}).  \
 \       HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \