# HG changeset patch
# User paulson
# Date 981468176 -3600
# Node ID f869d8617c81216387b7694e91dd401366a52d88
# Parent  b996b1857028b30441e989130605e06c2f1f3f9b
new theorem Transset_iff_Union_subset

diff -r b996b1857028 -r f869d8617c81 src/ZF/Ordinal.ML
--- 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]