1.1 --- a/src/ZF/AC/DC.thy	Mon Mar 12 23:33:50 2012 +0100
     1.2 +++ b/src/ZF/AC/DC.thy	Tue Mar 13 12:04:07 2012 +0000
     1.3 @@ -492,6 +492,13 @@
     1.4  lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
     1.5  by (fast elim!: image_fun [THEN ssubst])
     1.6  
     1.7 +lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
     1.8 +apply (unfold lesspoll_def)
     1.9 +apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
    1.10 +            intro!: eqpollI elim: notE
    1.11 +            elim!: eqpollE lepoll_trans)
    1.12 +done
    1.13 +
    1.14  theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) ==> WO3"
    1.15  apply (unfold DC_def WO3_def)
    1.16  apply (rule allI)