--- a/RTree.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/RTree.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -128,6 +128,21 @@
 locale fbranch =
   fixes r
   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
+begin
+
+lemma finite_children: "finite (children r x)"
+proof(cases "children r x = {}")
+  case True
+  thus ?thesis by auto
+next
+  case False
+  then obtain y where "(y, x) \<in> r" by (auto simp:children_def)
+  hence "x \<in> Range r" by auto
+  from fb[rule_format, OF this]
+  show ?thesis .
+qed
+
+end
 
 locale fsubtree = fbranch + 
    assumes wf: "wf r"