--- a/src/ZF/Epsilon.thy Sun Jun 16 11:58:54 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue Jun 18 10:51:04 2002 +0200
@@ -132,6 +132,9 @@
lemma under_Memrel: "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"
by (unfold Transset_def, blast)
+lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
+by (simp add: lt_def Ord_def under_Memrel)
+
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
--- 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: