new theorem Transset_iff_Union_subset

--- a/src/ZF/Ordinal.ML	Tue Feb 06 14:42:28 2001 +0100
+++ b/src/ZF/Ordinal.ML	Tue Feb 06 15:02:56 2001 +0100
@@ -8,7 +8,7 @@
 
 (*** Rules for Transset ***)
 
-(** Two neat characterisations of Transset **)
+(** Three neat characterisations of Transset **)
 
 Goalw [Transset_def] "Transset(A) <-> A<=Pow(A)";
 by (Blast_tac 1);
@@ -18,6 +18,10 @@
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Transset_iff_Union_succ";
 
+Goalw [Transset_def] "Transset(A) <-> Union(A) <= A";
+by (Blast_tac 1);
+qed "Transset_iff_Union_subset";
+
 (** Consequences of downwards closure **)
 
 Goalw [Transset_def]