# HG changeset patch
# User lcp
# Date 788197822 -3600
# Node ID 120edb26ee9322effcc54fc23b1fa59c1008f357
# Parent  778f0154666978fdf0b5a0b95645842229a257f0
Moved Transset_includes_summands and Transset_sum_Int_subset
here from Ordinal.ML

diff -r 778f01546669 -r 120edb26ee93 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Fri Dec 23 16:49:48 1994 +0100
+++ b/src/ZF/QUniv.ML	Fri Dec 23 16:50:22 1994 +0100
@@ -8,6 +8,21 @@
 
 open QUniv;
 
+(** Properties involving Transset and Sum **)
+
+val [prem1,prem2] = goalw QUniv.thy [sum_def]
+    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
+by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
+by (REPEAT (etac (prem1 RS Transset_includes_range) 1
+     ORELSE resolve_tac [conjI, singletonI] 1));
+qed "Transset_includes_summands";
+
+val [prem] = goalw QUniv.thy [sum_def]
+    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
+by (rtac (Int_Un_distrib RS ssubst) 1);
+by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
+qed "Transset_sum_Int_subset";
+
 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
 
 goalw QUniv.thy [quniv_def]