1.1 --- a/src/ZF/Ordinal.thy	Thu Jul 18 15:21:42 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Fri Jul 19 13:28:19 2002 +0200
     1.3 @@ -300,11 +300,16 @@
     1.4  apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) 
     1.5  done
     1.6  
     1.7 -(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
     1.8 +text{*The premise @{term "Ord(i)"} does not suffice.*}
     1.9  lemma trans_Memrel: 
    1.10      "Ord(i) ==> trans(Memrel(i))"
    1.11  by (unfold Ord_def Transset_def trans_def, blast)
    1.12  
    1.13 +text{*However, the following premise is strong enough.*}
    1.14 +lemma Transset_trans_Memrel: 
    1.15 +    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
    1.16 +by (unfold Transset_def trans_def, blast)
    1.17 +
    1.18  (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
    1.19  lemma Transset_Memrel_iff: 
    1.20      "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A"