src/ZF/Epsilon.thy
changeset 13387 b7464ca2ebbb
parent 13357 6f54e992777e
child 13524 604d0f3622d6
     1.1 --- a/src/ZF/Epsilon.thy	Wed Jul 17 16:41:32 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Thu Jul 18 10:37:55 2002 +0200
     1.3 @@ -116,6 +116,17 @@
     1.4  apply (rule subset_refl)
     1.5  done
     1.6  
     1.7 +text{*A transitive set either is empty or contains the empty set.*}
     1.8 +lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A --> 0\<in>A";
     1.9 +apply (simp add: Transset_def) 
    1.10 +apply (rule_tac a=x in eps_induct, clarify) 
    1.11 +apply (drule bspec, assumption) 
    1.12 +apply (rule_tac P = "x=0" in case_split_thm, auto)
    1.13 +done
    1.14 +
    1.15 +lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
    1.16 +by (blast dest: Transset_0_lemma)
    1.17 +
    1.18  
    1.19  subsection{*Epsilon Recursion*}
    1.20