[STATEMENT]
lemma inheritedJoinI[rule_format]: "[| inherited subs P; inherited subs Q; R = ( % x . P x & Q x) |] ==> inherited subs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inherited subs P; inherited subs Q; R = (\<lambda>x. P x \<and> Q x)\<rbrakk> \<Longrightarrow> inherited subs R
[PROOF STEP]
by(blast intro!:inheritedI dest: inheritedUnEq inheritedIncLevelEq inheritedInsertEq inheritedEmpty)