Theory topo_frontier_algebra

theory topo_frontier_algebra
  imports topo_operators_basic
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section β€ΉFrontier Algebraβ€Ί

textβ€Ή\noindent{The closure of a set A (@{text "π’ž(A)"}) can be seen as the set A augmented by (i) its boundary points,
or (ii) its accumulation/limit points. In this section we explore the first variant by drawing on the notion
of a frontier algebra, defined in an analogous fashion as the well-known closure and interior algebras.}β€Ί

textβ€Ή\noindent{Declares a primitive (unconstrained) frontier (aka. boundary) operation and defines others from it.}β€Ί
consts β„±::"Οƒβ‡’Οƒ"
abbreviation "ℐ ≑ ℐF β„±" ―‹ interior β€Ί
abbreviation "π’ž ≑ π’žF β„±" ―‹ closure β€Ί
abbreviation "ℬ ≑ ℬF β„±" ―‹ border β€Ί


subsection β€ΉBasic propertiesβ€Ί

textβ€Ή\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}β€Ί
lemma ICdual: "Fr_2 β„± ⟹ ℐ ≑ π’žd" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma ICdual': "Fr_2 β„± ⟹ π’ž ≑ ℐd" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma BI_rel: "ℬ ≑ ℬI ℐ" using Br_fr_def Br_int_def Int_fr_def unfolding equal_op_def conn by auto
lemma IB_rel: "ℐ ≑ ℐB ℬ" using Br_fr_def Int_br_def Int_fr_def unfolding equal_op_def conn by auto
lemma BC_rel: "Fr_2 β„± ⟹ ℬ ≑ ℬC π’ž"  using BI_BC_rel BI_rel ICdual' eq_ext' by fastforce
lemma CB_rel: "Fr_2 β„± ⟹ π’ž ≑ π’žB ℬ" using Br_fr_def Cl_br_def Cl_fr_def Fr_2_def unfolding equal_op_def conn by auto
lemma FI_rel: "Fr_2 β„± ⟹ β„± ≑ β„±I ℐ" by (smt Cl_fr_def Fr_int_def ICdual' Int_fr_def compl_def diff_def equal_op_def join_def meet_def)
lemma FC_rel: "Fr_2 β„± ⟹ β„± ≑ β„±C π’ž" by (metis (mono_tags, lifting) FI_rel Fr_2_def Fr_cl_def Fr_int_def ICdual' dual_def eq_ext' equal_op_def)
lemma FB_rel: "Fr_2 β„± ⟹ β„± ≑ β„±B ℬ" by (smt Br_fr_def CB_rel Cl_br_def FC_rel Fr_br_def Fr_cl_def equal_op_def join_def meet_def)

textβ€Ή\noindent{Fixed-point and other operators are interestingly related.}β€Ί
lemma fp1: "ℐfp ≑ ℬc" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp2: "ℬfp ≑ ℐc" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto 
lemma fp3: "Fr_2 β„± ⟹ π’žfp ≑ ℬd" using Br_fr_def Cl_fr_def Fr_2_def dual_def equal_op_def conn by fastforce
lemma fp4: "Fr_2 β„± ⟹ (ℬd)fp ≑ π’ž" by (smt dimp_def equal_op_def fp3)
lemma fp5: "β„±fp ≑ ℬ βŠ” (π’žc)" using Br_fr_def Cl_fr_def unfolding equal_op_def conn by auto

textβ€Ή\noindent{Different inter-relations (some redundant ones are kept to help the provers).}β€Ί
lemma monI: "Fr_1b β„± ⟹ MONO(ℐ)" by (simp add: IF1a MONO_MULTa)
lemma monC: "Fr_6 β„± ⟹ MONO(π’ž)" by (simp add: Cl_fr_def Fr_6_def MONO_def conn)
lemma pB1: "βˆ€A. ℬ A β‰ˆ A β†Ό ℐ A" using Br_fr_def fp1 unfolding conn equal_op_def by metis
lemma pB2: "βˆ€A. ℬ A β‰ˆ A ∧ β„± A" by (simp add: Br_fr_def)
lemma pB3: "Fr_2 β„± ⟹ βˆ€A. ℬ(─A) β‰ˆ ─A ∧ β„± A" by (simp add: Fr_2_def pB2 conn)
lemma pB4: "Fr_2 β„± ⟹ βˆ€A. ℬ(─A) β‰ˆ ─A ∧ π’ž A" using CB_rel Cl_br_def pB3 unfolding conn equal_op_def by metis
lemma pB5: "Fr_1b β„± ⟹ Fr_2 β„± ⟹ βˆ€A. ℬ(π’ž A) β‰Ό (ℬ A) ∨ ℬ(─A)"  by (smt BC_rel Br_cl_def Cl_fr_def Fr_6_def PF6 equal_op_def conn)
lemma pF1: "βˆ€A. β„± A β‰ˆ π’ž A β†Ό ℐ A"  using Cl_fr_def Int_fr_def conn by auto
lemma pF2: "Fr_2 β„± ⟹ βˆ€A. β„± A β‰ˆ π’ž A ∧ π’ž(─A)" using Cl_fr_def Fr_2_def conn by auto
lemma pF3: "Fr_2 β„± ⟹ βˆ€A. β„± A β‰ˆ ℬ A ∨ ℬ(─A)" using Br_fr_def Fr_2_def conn by auto
lemma pF4: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4(β„±) ⟹ βˆ€A. β„±(ℐ A) β‰Ό β„± A" by (smt IDEMa_def IF2 IF4 Int_fr_def MONO_def PF1 PF6 PI4 diff_def monC pF1)
lemma pF5: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A. β„±(π’ž A) β‰Ό β„± A" by (metis Br_fr_def CF4 Cl_fr_def IDEM_def PF1 join_def meet_def pB5 pF3)
lemma pA1: "βˆ€A. A β‰ˆ ℐ A ∨ ℬ A" using Br_fr_def Int_fr_def unfolding conn by auto
lemma pA2: "Fr_2 β„± ⟹ βˆ€A. A β‰ˆ π’ž A β†Ό ℬ(─A)" using pB1 dual_def fp3 unfolding equal_op_def conn by smt 
lemma pC1: "Fr_2 β„± ⟹ βˆ€A. π’ž A β‰ˆ A ∨ ℬ(─A)" using Cl_fr_def pB4 conn by auto
lemma pC2: "βˆ€A. π’ž A β‰ˆ A ∨ β„± A" using Cl_fr_def by auto
lemma pI1: "βˆ€A. ℐ A β‰ˆ A β†Ό ℬ A" using pA1 pB1 conn by auto
lemma pI2: "βˆ€A. ℐ A β‰ˆ A β†Ό β„± A" by (simp add: Int_fr_def)

lemma IC_imp: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_3 β„± ⟹ βˆ€A B. ℐ(A β†’ B) β‰Ό π’ž A β†’ π’ž B" proof -
  assume fr1: "Fr_1 β„±" and fr2: "Fr_2 β„±" and fr3: "Fr_3 β„±"
  { fix a b
    have "(a β†’ b) ∧ ─b β†’ ─a = ⊀" unfolding conn by auto
    hence "ℐ((a β†’ b) ∧ ─b β†’ ─a) β‰ˆ ℐ(⊀)" by simp
    hence "ℐ((a β†’ b) ∧ ─b β†’ ─a) β‰ˆ ⊀" using fr3 IF3 dNOR_def fr2 by auto
    moreover have "let A=(a β†’ b) ∧ ─b; B=─a in ℐ(A β†’ B) β‰Ό ℐ(A) β†’ ℐ(B)" using fr1 IF1 PI7 Int_7_def by metis
    ultimately have "ℐ((a β†’ b) ∧ ─b) β†’ ℐ(─a) β‰ˆ ⊀" unfolding conn by simp
    moreover have "let A=a β†’ b; B=─b in ℐ(A ∧ B) β‰ˆ ℐ(A) ∧ ℐ(B)" using fr1 IF1 MULT_def by simp
    ultimately have "ℐ(a β†’ b) ∧ ℐ(─b) β†’ ℐ(─a) β‰ˆ ⊀" unfolding conn by simp
    moreover have "βˆ€A. ℐ(─A) β‰ˆ β”€π’ž(A)" using Cl_fr_def Fr_2_def Int_fr_def fr2  unfolding conn by auto
    ultimately have "ℐ(a β†’ b) ∧ β”€π’ž(b) β†’ β”€π’ž(a) β‰ˆ ⊀" unfolding conn by simp
    hence "ℐ(a β†’ b) ∧ β”€π’ž(b) β‰Ό β”€π’ž(a)" unfolding conn by simp
    hence "ℐ(a β†’ b) ∧ π’ž a β‰Ό π’ž b" unfolding conn by metis
  } thus ?thesis unfolding conn by simp
qed

textβ€Ή\noindent{Defines some fixed-point predicates and prove some properties.}β€Ί
abbreviation openset ("Op") where "Op A ≑ fp ℐ A"
abbreviation closedset ("Cl") where "Cl A ≑ fp π’ž A"
abbreviation borderset ("Br") where "Br A ≑ fp ℬ A"
abbreviation frontierset ("Fr") where "Fr A ≑ fp β„± A"

lemma Int_Open: "Fr_1a β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A. Op(ℐ A)" using IF4 IDEM_def by blast
lemma Cl_Closed: "Fr_1a β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A. Cl(π’ž A)" using CF4 IDEM_def by blast
lemma Br_Border: "Fr_1b β„± ⟹ βˆ€A. Br(ℬ A)" using Br_fr_def Fr_1b_def conn by auto
textβ€Ή\noindent{In contrast, there is no analogous fixed-point result for frontier:}β€Ί
lemma "𝔉 β„± ⟹ βˆ€A. Fr(β„± A)" nitpick oops (*counterexample even if assuming all frontier conditions*)

lemma OpCldual: "Fr_2 β„± ⟹ βˆ€A. Cl A ⟷ Op(─A)" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
lemma ClOpdual: "Fr_2 β„± ⟹ βˆ€A. Op A ⟷ Cl(─A)" using ICdual dual_def unfolding equal_op_def conn by auto
lemma Fr_ClBr: "βˆ€A. Fr(A) = (Cl(A) ∧ Br(A))" using Br_fr_def Cl_fr_def join_def meet_def by auto
lemma Cl_F: "Fr_4 β„± ⟹ βˆ€A. Cl(β„± A)" using Cl_fr_def Fr_4_def conn by auto


subsection β€ΉFurther propertiesβ€Ί

textβ€Ή\noindent{The definitions and theorems below are well known in the literature (e.g. @{cite Kuratowski2}).
Here we uncover the minimal conditions under which they hold (taking frontier operation as primitive).}β€Ί
lemma Cl_Bzero: "Fr_2 β„± ⟹ βˆ€A. Cl A ⟷ ℬ(─A) β‰ˆ βŠ₯" using pA2 pC1 unfolding conn by metis
lemma Op_Bzero: "βˆ€A. Op A ⟷ (ℬ A) β‰ˆ βŠ₯" using pB1 pI1 unfolding conn by metis
lemma Br_boundary: "Fr_2 β„± ⟹ βˆ€A. Br(A) ⟷ ℐ A β‰ˆ βŠ₯" by (metis Br_fr_def Int_fr_def bottom_def diff_def meet_def)
lemma Fr_nowhereDense: "Fr_2 β„± ⟹ βˆ€A. Fr(A) ⟢ ℐ(π’ž A) β‰ˆ βŠ₯" using Fr_ClBr Br_boundary eq_ext by metis
lemma Cl_FB: "βˆ€A. Cl A ⟷ β„± A β‰ˆ ℬ A" using Br_fr_def Cl_fr_def unfolding conn by auto
lemma Op_FB: "Fr_2 β„± ⟹ βˆ€A. Op A ⟷ β„± A β‰ˆ ℬ(─A)" using Br_fr_def Fr_2_def Int_fr_def unfolding conn by auto
lemma Clopen_Fzero: "βˆ€A. Cl A ∧ Op A ⟷ β„± A β‰ˆ βŠ₯" using Cl_fr_def Int_fr_def unfolding conn by auto

lemma Int_sup_closed: "Fr_1b β„± ⟹ supremum_closed (Ξ»A. Op A)" by (smt IF1a Int_fr_def MONO_def MONO_MULTa sup_char conn)
lemma Int_meet_closed: "Fr_1a β„± ⟹ meet_closed (Ξ»A. Op A)" using Fr_1a_def Int_fr_def unfolding conn by metis
lemma Int_inf_closed: "Fr_inf β„± ⟹ infimum_closed (Ξ»A. Op A)" by (simp add: fp_IF_inf_closed)
lemma Cl_inf_closed: "Fr_6 β„± ⟹ infimum_closed (Ξ»A. Cl A)" by (smt Cl_fr_def Fr_6_def infimum_def join_def)
lemma Cl_join_closed: "Fr_1a β„± ⟹ Fr_2 β„± ⟹ join_closed (Ξ»A. Cl A)" using ADDI_a_def CF1a CF2 EXP_def unfolding conn by metis
lemma Cl_sup_closed: "Fr_2 β„± ⟹ Fr_inf β„± ⟹ supremum_closed (Ξ»A. Cl A)" by (simp add: fp_CF_sup_closed)
lemma Br_inf_closed: "Fr_1b β„± ⟹ infimum_closed (Ξ»A. Br A)" by (smt BI_rel Br_int_def IF1a MONO_iMULTa MONO_MULTa Ra_restr_all eq_ext' iMULT_a_def inf_char diff_def)
lemma Fr_inf_closed: "Fr_1b β„± ⟹ Fr_2 β„± ⟹ infimum_closed (Ξ»A. Fr A)" by (metis (full_types) Br_fr_def Br_inf_closed PF6 Cl_fr_def Cl_inf_closed meet_def join_def)
lemma Br_Fr_join: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A B. Br A ∧ Fr B ⟢ Br(A ∨ B)" proof -
  assume fr1: "Fr_1 β„±" and fr2: "Fr_2 β„±" and fr4: "Fr_4 β„±"
  { fix A B
    { assume bra: "Br A" and frb: "Fr B"
      from bra have "ℐ A β‰ˆ βŠ₯" using Br_boundary fr2 by auto
      hence 1: "π’ž(─A) β‰ˆ ⊀" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
      from frb have "ℐ(π’ž B) β‰ˆ βŠ₯" by (simp add: Fr_nowhereDense fr2)
      hence 2: "π’ž(─(π’ž B)) β‰ˆ ⊀" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
      from fr1 fr2 have "π’ž(─A) β†Ό π’ž B β‰Ό π’ž((─A) β†Ό B)" using CF1 Cl_6_def PC6 by metis
      hence "π’ž(─A) β†Ό π’ž B β‰Ό π’ž(─(A ∨ B))" unfolding conn by simp
      hence "⊀ β†Ό π’ž B β‰Ό π’ž(─(A ∨ B))" using 1 unfolding conn by simp
      hence 3: "─(π’ž B) β‰Ό π’ž(─(A ∨ B))" unfolding conn by simp
      from fr1 fr2 fr4 have 4: "let M=─(π’ž B); N=─(A ∨ B) in  M β‰Ό π’ž N ⟢ π’ž M β‰Ό π’ž N" using PC9 CF4 Cl_9_def PF1 CF1b by fastforce
      from 3 4 have "π’ž(─(π’ž B)) β‰Ό π’ž(─(A ∨ B))" by simp 
      hence "⊀ β‰ˆ π’ž(─(A ∨ B))" using 2 unfolding top_def by simp
      hence "βŠ₯ β‰ˆ ℐ(A ∨ B)" using fr2 ICdual dual_def eq_ext' conn by metis
      hence "Br (A ∨ B)" using fr2 Br_boundary by simp
    } hence "Br A ∧ Fr B ⟢ Br (A ∨ B)" by simp
  } hence "βˆ€A B. Br A ∧ Fr B ⟢ Br (A ∨ B)" by simp
  thus ?thesis by simp
qed
lemma Fr_join_closed: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ join_closed (Ξ»A. Fr A)" by (smt Br_Fr_join ADDI_a_def CF1a Cl_fr_def PF1 diff_def join_def meet_def pB2 pF1)


textβ€Ή\noindent{Introduces a predicate for indicating that two sets are disjoint and proves some properties.}β€Ί
abbreviation "Disj A B ≑ A ∧ B β‰ˆ βŠ₯" 

lemma Disj_comm: "βˆ€A B. Disj A B ⟢ Disj B A" unfolding conn by fastforce
lemma Disj_IF: "βˆ€A. Disj (ℐ A) (β„± A)" by (simp add: Int_fr_def conn)
lemma Disj_B: "βˆ€A. Disj (ℬ A) (ℬ(─A))" using Br_fr_def unfolding conn by auto
lemma Disj_I: "βˆ€A. Disj (ℐ A) (─A)" by (simp add: Int_fr_def conn)
lemma Disj_BCI: "Fr_2 β„± ⟹ βˆ€A. Disj (ℬ(π’ž A)) (ℐ(─A))" using Br_fr_def Cl_fr_def Fr_2_def Int_fr_def conn by metis
lemma Disj_CBI: "Fr_6 β„± ⟹ Fr_4 β„± ⟹ βˆ€A. Disj (π’ž(ℬ(─A))) (ℐ(─A))" by (metis Br_fr_def Cl_F IB_rel Int_br_def MONO_MULTa MULT_a_def eq_ext' monC conn)

textβ€Ή\noindent{Introduces a predicate for indicating that two sets are separated and proves some properties.}β€Ί
definition "Sep A B ≑ Disj (π’ž A) B ∧ Disj (π’ž B) A"

lemma Sep_comm: "βˆ€A B. Sep A B ⟢ Sep B A" by (simp add: Sep_def)
lemma Sep_disj: "βˆ€A B. Sep A B ⟢ Disj A B" using Cl_fr_def Sep_def conn by fastforce
lemma Sep_I: "Fr_1(β„±) ⟹ Fr_2(β„±) ⟹ Fr_4(β„±) ⟹ βˆ€A. Sep (ℐ A) (ℐ (─A))" using Cl_fr_def pF4 Fr_2_def Int_fr_def unfolding Sep_def conn by metis
lemma Sep_sub: "Fr_6 β„±  ⟹ βˆ€A B C D. Sep A B ∧ C β‰Ό A ∧ D β‰Ό B ⟢ Sep C D" using MONO_def monC unfolding Sep_def conn by smt
lemma Sep_Cl_diff: "Fr_6 β„± ⟹ βˆ€A B. Cl(A) ∧ Cl(B) ⟢ Sep (A β†Ό B) (B β†Ό A)" using Fr_6_def pC2 unfolding Sep_def conn by smt
lemma Sep_Op_diff: "Fr_1b β„± ⟹ Fr_2 β„± ⟹ βˆ€A B. Op(A) ∧ Op(B) ⟢ Sep (A β†Ό B) (B β†Ό A)" proof - 
  assume fr1b:"Fr_1b β„±" and fr2:"Fr_2 β„±"
  { fix A B 
    from fr1b fr2 have aux: "let M=─A ; N=─B in (Cl(M) ∧ Cl(N) ⟢ Sep (M β†Ό N) (N β†Ό M))" using PF6 Sep_Cl_diff by simp
    { assume "Op(A) ∧ Op(B)"
      hence "Cl(─A) ∧ Cl(─B)" using fr2 ClOpdual by simp
      hence "Sep (─A β†Ό ─B) (─B β†Ό ─A)" using fr1b fr2 aux unfolding conn by simp
      moreover have "(─A β†Ό ─B) β‰ˆ (B β†Ό A)" unfolding conn by auto
      moreover have "(─B β†Ό ─A) β‰ˆ (A β†Ό B)" unfolding conn by auto
      ultimately have "Sep (B β†Ό A) (A β†Ό B)" unfolding conn by simp
      hence "Sep (A β†Ό B) (B β†Ό A)" using Sep_comm by simp
    } hence "Op(A) ∧ Op(B) ⟢ Sep (A β†Ό B) (B β†Ό A)" by (rule impI)
  } thus ?thesis by simp
qed
lemma Sep_Cl: "βˆ€A B. Cl(A) ∧ Cl(B) ∧ Disj A B ⟢ Sep A B" unfolding Sep_def conn by blast
lemma Sep_Op: "Fr_1b β„± ⟹ Fr_2 β„±  ⟹ βˆ€A B. Op(A) ∧ Op(B) ∧ Disj A B ⟢ Sep A B" proof -
  assume fr1b:"Fr_1b β„±" and fr2:"Fr_2 β„±"
  { fix A B 
    from fr1b fr2 have aux: "Op(A) ∧ Op(B) ⟢ Sep (A β†Ό B) (B β†Ό A)" using Sep_Op_diff by simp
    { assume op: "Op(A) ∧ Op(B)" and disj: "Disj A B"
      hence "(A β†Ό B) β‰ˆ A ∧ (B β†Ό A) β‰ˆ B" unfolding conn by blast
      hence "Sep A B" using op aux unfolding conn by simp
    } hence "Op(A) ∧ Op(B) ∧ Disj A B ⟢ Sep A B" by simp
  } thus ?thesis by simp
qed
lemma "Fr_1a β„± ⟹ Fr_2 β„± ⟹ βˆ€A B C. Sep A B ∧ Sep A C ⟢ Sep A (B ∨ C)" using CF1a ADDI_a_def unfolding Sep_def conn by metis


textβ€Ή\noindent{Verifies a neighborhood-based definition of closure.}β€Ί
definition "nbhd A p ≑ βˆƒE. E β‰Ό A ∧ Op(E) ∧ (E p)"
lemma nbhd_def2: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A p. (nbhd A p) = (ℐ A p)" using pF4 MONO_def PF1 monI pI2 unfolding nbhd_def conn by smt

lemma C_def_lr: "Fr_1b β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A p. (π’ž A p) ⟢ (βˆ€E. (nbhd E p) ⟢ Β¬(Disj E A))" using Cl_fr_def Fr_2_def Fr_6_def PF6 pF1 unfolding nbhd_def conn by smt
lemma C_def_rl: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A p. (π’ž A p) ⟡ (βˆ€E. (nbhd E p) ⟢ Β¬(Disj E A))" using Cl_fr_def pF5 pA1 pB4 unfolding nbhd_def conn by smt
lemma C_def: "Fr_1 β„± ⟹ Fr_2 β„± ⟹ Fr_4 β„± ⟹ βˆ€A p. (π’ž A p) ⟷ (βˆ€E. (nbhd E p) ⟢ Β¬(Disj E A))" using C_def_lr C_def_rl PF1 by blast


textβ€Ή\noindent{Explore the Barcan and converse Barcan formulas.}β€Ί
lemma Barcan_I: "Fr_inf β„± ⟹ βˆ€P. (βˆ€x. ℐ(P x)) β‰Ό ℐ(βˆ€x. P x)" using IF_inf Barcan1 by auto
lemma Barcan_C: "Fr_2 β„± ⟹ Fr_inf β„± ⟹ βˆ€P. π’ž(βˆƒx. P x) β‰Ό (βˆƒx. π’ž(P x))" using Fr_2_def CF_inf Barcan2 by metis
lemma CBarcan_I: "Fr_1b β„± ⟹ βˆ€P. ℐ(βˆ€x. P x)  β‰Ό (βˆ€x. ℐ(P x))" by (metis (mono_tags, lifting) MONO_def monI)
lemma CBarcan_C: "Fr_6 β„± ⟹ βˆ€P. (βˆƒx. π’ž(P x)) β‰Ό π’ž(βˆƒx. P x)"  by (metis (mono_tags, lifting) MONO_def monC)

end