[STATEMENT]
lemma (in Group) rcs_sub_smult:"\<lbrakk>G \<guillemotright> H; G \<guillemotright> N; a \<in> H\<rbrakk> \<Longrightarrow> N \<bullet> a \<subseteq> N \<diamondop>\<^bsub>G\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<guillemotright> H ; G \<guillemotright> N ; a \<in> H\<rbrakk> \<Longrightarrow> N \<bullet> a \<subseteq> N \<diamondop> H
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>G \<guillemotright> H ; G \<guillemotright> N ; a \<in> H; x \<in> N \<bullet> a\<rbrakk> \<Longrightarrow> x \<in> N \<diamondop> H
[PROOF STEP]
apply (simp add:rcs_def s_top_def, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done