| changeset 16417 | 9bc16273c2d4 |
| parent 13339 | 0f89104dd377 |
| child 32960 | 69916a850301 |
--- a/src/ZF/AC/Cardinal_aux.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/AC/Cardinal_aux.thy Fri Jun 17 16:12:49 2005 +0200 @@ -5,7 +5,7 @@ Auxiliary lemmas concerning cardinalities *) -theory Cardinal_aux = AC_Equiv: +theory Cardinal_aux imports AC_Equiv begin lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m" apply (rule not_emptyE, assumption)