src/ZF/WF.thy

--- a/src/ZF/WF.thy	Sun Jun 16 11:58:54 2002 +0200
+++ b/src/ZF/WF.thy	Tue Jun 18 10:51:04 2002 +0200
@@ -66,6 +66,9 @@
 lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
 by (unfold wf_on_def wf_def, fast)
 
+lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
+by (simp add: wf_def, fast)
+
 (** Introduction rules for wf_on **)
 
 lemma wf_onI: