[STATEMENT]
lemma "Fr_2 \<F> \<Longrightarrow> \<forall>A B. Cl(A) \<longrightarrow> CoP3\<^sup>A\<^sup>B \<^bold>\<not>\<^sup>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A. contains (\<lambda>B. contains A B \<longleftarrow> contains (\<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I A)) (\<lambda>B. \<forall>w. \<C> A w = A w)
[PROOF STEP]
by (metis Disj_I ICdual' compl_def dual_def eq_ext' meet_def neg_I_def)