subsetD;

--- a/src/HOL/Calculation.thy	Wed Sep 29 16:41:52 1999 +0200
+++ b/src/HOL/Calculation.thy	Wed Sep 29 16:44:18 1999 +0200
@@ -17,6 +17,12 @@
 
 theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)
 
+theorem [trans]: "[| c:A; A <= B |] ==> c:B";
+  by (rule subsetD);
+
+theorem [trans]: "[| A <= B; c:A |] ==> c:B";
+  by (rule subsetD);
+
 theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y";     (*  ~=  <=  < *)
   by (simp! add: order_less_le);