diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/Order.ML	Tue Jul 26 13:21:20 1994 +0200
@@ -25,6 +25,31 @@
 by (fast_tac ZF_cs 1);
 val part_ord_Imp_asym = result();
 
+(** Subset properties for the various forms of relation **)
+
+
+(*Note: a relation s such that s<=r need not be a partial ordering*)
+goalw Order.thy [part_ord_def, irrefl_def, trans_on_def]
+    "!!A B r. [| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
+by (fast_tac ZF_cs 1);
+val part_ord_subset = result();
+
+goalw Order.thy [linear_def]
+    "!!A B r. [| linear(A,r);  B<=A |] ==> linear(B,r)";
+by (fast_tac ZF_cs 1);
+val linear_subset = result();
+
+goalw Order.thy [tot_ord_def]
+    "!!A B r. [| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)";
+by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1);
+val tot_ord_subset = result();
+
+goalw Order.thy [well_ord_def]
+    "!!A B r. [| well_ord(A,r);  B<=A |] ==> well_ord(B,r)";
+by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1);
+val well_ord_subset = result();
+
+
 (** Order-isomorphisms **)
 
 goalw Order.thy [ord_iso_def] 
@@ -169,7 +194,6 @@
 by (safe_tac ZF_cs);
 val well_ord_is_trans_on = result();
 
-
 (*** Derived rules for pred(A,x,r) ***)
 
 val [major,minor] = goalw Order.thy [pred_def]