[STATEMENT]
lemma "Fr_2 \<F> \<Longrightarrow> \<forall>A B. Cl(A) \<and> Cl(B) \<longrightarrow> DM1\<^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 (\<^bold>\<not>\<^sup>I A \<^bold>\<and> \<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I (A \<^bold>\<or> B))) (\<lambda>B. (\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<C> B w = B w))
[PROOF STEP]
using pF2 pI2 conn
[PROOF STATE]
proof (prove)
using this:
Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<F> A w = (\<C> A \<^bold>\<and> \<C> (\<^bold>\<midarrow>A)) w
\<forall>A w. \<I> A w = (A \<^bold>\<leftharpoonup> \<F> A) w
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
\<^bold>\<not>\<^sup>I ?\<phi> \<equiv> \<I> (\<^bold>\<midarrow>?\<phi>)
\<^bold>\<not>\<^sup>C ?\<phi> \<equiv> \<C> (\<^bold>\<midarrow>?\<phi>)

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A. contains (\<lambda>B. contains (\<^bold>\<not>\<^sup>I A \<^bold>\<and> \<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I (A \<^bold>\<or> B))) (\<lambda>B. (\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<C> B w = B w))
[PROOF STEP]
by fastforce