a new theorem

--- a/src/HOL/UNITY/Comp.ML	Mon Aug 30 11:13:27 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Mon Aug 30 11:20:23 1999 +0200
@@ -71,6 +71,10 @@
 by (Blast_tac 1);
 qed "Join_component_iff";
 
+Goal "[| F component G; G : A co B |] ==> F : A co B";
+by (auto_tac (claset(), 
+	      simpset() addsimps [constrains_def, component_eq_subset]));
+qed "component_constrains";
 
 (*** existential properties ***)