[STATEMENT]
lemma sqUn_lem3: "\<lbrakk> A \<sqsubseteq> A'; B \<sqsubseteq> B' \<rbrakk> \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> A'; B \<sqsubseteq> B'\<rbrakk> \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B'
[PROOF STEP]
by(auto simp add: hyperset_defs)