--- a/RTree.thy	Tue Dec 15 15:10:40 2015 +0000
+++ b/RTree.thy	Fri Dec 18 19:13:19 2015 +0800
@@ -489,7 +489,7 @@
   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]
   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis
   thus ?thesis by (simp add: pred_of_star star_2_pstar)
-qed
+qed  
 
 lemma subtree_transfer:
   assumes "a \<in> subtree r1 a'"
@@ -564,6 +564,13 @@
   shows "a \<in> subtree r b"
   using assms by (auto simp:subtree_def ancestors_def)
 
+lemma ancestors_Field:
+  assumes "b \<in> ancestors r a"
+  obtains "a \<in> Domain r" "b \<in> Range r"
+  using assms 
+  apply (unfold ancestors_def, simp)
+  by (metis Domain.DomainI Range.intros trancl_domain trancl_range)
+
 lemma subtreeE:
   assumes "a \<in> subtree r b"
   obtains "a = b"