--- a/RTree.thy	Tue Dec 22 23:13:31 2015 +0800
+++ b/RTree.thy	Wed Jan 06 20:46:14 2016 +0800
@@ -597,6 +597,23 @@
   with that[unfolded ancestors_def] show ?thesis by auto
 qed
 
+
+lemma subtree_Field:
+  "subtree r x \<subseteq> Field r \<union> {x}"
+proof
+  fix y
+  assume "y \<in> subtree r x"
+  thus "y \<in> Field r \<union> {x}"
+  proof(cases rule:subtreeE)
+    case 1
+    thus ?thesis by auto
+  next
+    case 2
+    thus ?thesis apply (auto simp:ancestors_def)
+    using Field_def tranclD by fastforce 
+  qed
+qed
+
 lemma subtree_ancestorsI:
   assumes "a \<in> subtree r b"
   and "a \<noteq> b"