[STATEMENT]
lemma "Der_1b \<D> \<Longrightarrow> Der_3 \<D> \<Longrightarrow> MT1(\<^bold>\<not>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Der_1b \<D>; Fr_3 \<D>\<rbrakk> \<Longrightarrow> MT1 \<^bold>\<not>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Der_1b \<D>; Fr_3 \<D>\<rbrakk> \<Longrightarrow> \<forall>a. contains (\<lambda>b. [\<^bold>\<turnstile> \<lambda>w. \<^bold>\<not> a w = \<^bold>\<top> w]) (\<lambda>b. contains (\<^bold>\<not> b) a \<and> [\<^bold>\<turnstile> \<lambda>w. b w = \<^bold>\<top> w])
[PROOF STEP]
by (metis (full_types) NOR_def PD1 bottom_def compl_def diff_def ineg_prop top_def)