diff --git a/Core_DOM/Core_DOM_Functions.thy b/Core_DOM/Core_DOM_Functions.thy
index 402c967..f279d89 100644
--- a/Core_DOM/Core_DOM_Functions.thy
+++ b/Core_DOM/Core_DOM_Functions.thy
@@ -3670,6 +3670,30 @@ lemma get_element_by_id_result_in_tree_order:
                intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
                split: option.splits list.splits if_splits)
 
+lemma get_elements_by_class_name_result_in_tree_order:
+  assumes "h \<turnstile> get_elements_by_class_name ptr name \<rightarrow>\<^sub>r results"
+  assumes "h \<turnstile> to_tree_order ptr \<rightarrow>\<^sub>r to"
+  assumes "element_ptr \<in> set results"
+  shows "cast element_ptr \<in> set to"
+  using assms 
+  by(auto simp add: get_elements_by_class_name_def first_in_tree_order_def  
+               elim!: map_filter_M_pure_E[where y=element_ptr]  bind_returns_result_E2 
+               dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] 
+               intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
+               split: option.splits list.splits if_splits)
+
+lemma get_elements_by_tag_name_result_in_tree_order:
+  assumes "h \<turnstile> get_elements_by_tag_name ptr name \<rightarrow>\<^sub>r results"
+  assumes "h \<turnstile> to_tree_order ptr \<rightarrow>\<^sub>r to"
+  assumes "element_ptr \<in> set results"
+  shows "cast element_ptr \<in> set to"
+  using assms 
+  by(auto simp add: get_elements_by_tag_name_def first_in_tree_order_def  
+               elim!: map_filter_M_pure_E[where y=element_ptr]  bind_returns_result_E2 
+               dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] 
+               intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
+               split: option.splits list.splits if_splits)
+
 lemma get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag_name) h"
   by(auto simp add: get_elements_by_tag_name_def 
           intro!: bind_pure_I map_filter_M_pure