[STATEMENT]
lemma (in Semilat) closed_f [simp, intro]: "\<lbrakk>x \<in> A; y \<in> A\<rbrakk>  \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> A
[PROOF STEP]
by (simp add: closedD [OF closedI])