src/ZF/ord.ML

 val Ord_succ = result();
 
 goal Ord.thy "Ord(succ(i)) <-> Ord(i)";
 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
 val Ord_succ_iff = result();
+
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
+by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
+val Ord_Un = result();
+
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
+by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
+val Ord_Int = result();
 
 val nonempty::prems = goal Ord.thy
     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
 by (rtac Ord_is_Transset 1);

 by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
 val succ_le_iff = result();
 
 (** Union and Intersection **)
 
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
+by (rtac (Un_upper1 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper1_le = result();
+
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
+by (rtac (Un_upper2 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper2_le = result();
+
 (*Replacing k by succ(k') yields the similar rule for le!*)
 goal Ord.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
 by (rtac (Un_commute RS ssubst) 4);
 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);