[STATEMENT]
lemma less_sets_Un1: "less_sets (A \<union> A') B \<longleftrightarrow> A \<lless> B \<and> A' \<lless> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<union> A' \<lless> B) = (A \<lless> B \<and> A' \<lless> B)
[PROOF STEP]
by (auto simp: less_sets_def)