Theory Topology_ZF_properties_3

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2013 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section ‹Properties in Topology 3›

theory Topology_ZF_properties_3 imports Topology_ZF_7 Finite_ZF_1 Topology_ZF_1b Topology_ZF_9
  Topology_ZF_properties_2 FinOrd_ZF
begin

text‹This theory file deals with more topological properties and the
relation with the previous ones in other theory files.›

subsection‹More anti-properties›

text‹In this section we study more anti-properties.›

subsection‹First examples›

text‹A first example of an anti-compact space is the discrete space.›

lemma pow_compact_imp_finite:
  assumes "B{is compact in}Pow(A)"
  shows "Finite(B)"
proof-
  from assms have B:"B⊆A" "∀M∈Pow(Pow(A)). B⊆⋃M ⟶(∃N∈FinPow(M). B⊆⋃N)"
    unfolding IsCompact_def by auto
  from B(1) have "{{x}. x∈B}∈Pow(Pow(A))" "B⊆⋃{{x}. x∈B}" by auto
  with B(2) have "∃N∈FinPow({{x}. x∈B}). B⊆⋃N" by auto
  then obtain N where "N∈FinPow({{x}. x∈B})" "B⊆⋃N" by auto
  then have "Finite(N)" "N⊆{{x}. x∈B}" "B⊆⋃N" unfolding FinPow_def by auto
  then have "Finite(N)" "∀b∈N. Finite(b)" "B⊆⋃N" by auto
  then have "B⊆⋃N" "Finite(⋃N)" using Finite_Union[of "N"] by auto
  then show "Finite(B)" using subset_Finite by auto
qed
    
theorem pow_anti_compact:
  shows "Pow(A){is anti-compact}"
proof-
  {
    fix B assume as:"B⊆⋃Pow(A)" "(⋃(Pow(A){restricted to}B)){is compact in}(Pow(A){restricted to}B)"
    then have sub:"B⊆A" by auto
    then have "Pow(B)=Pow(A){restricted to}B" unfolding RestrictedTo_def by blast
    with as(2) have "(⋃Pow(B)){is compact in}Pow(B)" by auto
    then have "B{is compact in}Pow(B)" by auto
    then have "Finite(B)" using pow_compact_imp_finite by auto
    then have "B{is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
  }
  then show ?thesis unfolding IsAntiComp_def antiProperty_def by auto
qed

text‹In a previous file, @{file "Topology_ZF_5.thy"}, we proved that
the spectrum of the lindelöf property depends on the axiom of countable choice
on subsets of the power set of the natural number.›

text‹In this context, the examples depend on wether this choice principle holds or not.
This is the reason that the examples of anti-lindeloef topologies are left for the next
section.›

subsection‹Structural results›

text‹We first differenciate the spectrum of the lindeloef property depending
on some axiom of choice.›

lemma lindeloef_spec1:
  assumes "{the axiom of} nat {choice holds for subsets}(Pow(nat))"
  shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ (A≲nat)"
  using compactK_spectrum[OF assms Card_nat] unfolding IsLindeloef_def.

lemma lindeloef_spec2:
  assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)))"
  shows "(A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))) ⟷ Finite(A)"
proof
  assume "Finite(A)"
  then have A:"A{is in the spectrum of} (λT. ((⋃T){is compact in}T))" using compact_spectrum by auto
  have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto
  {
    fix T assume "T{is a topology}" "(⋃T){is compact in}T"
    then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
    then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto
    then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto
  }
  then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto
  with A show "A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using P_imp_Q_spec_inv[
    where Q="λT. ((⋃T){is compact in}T)" and P="λT. ((⋃T){is lindeloef in}T)"] by auto
next
  assume A:"A {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))"
  then have reg:"∀T. T{is a topology}∧⋃T≈A ⟶ ((⋃T){is compact of cardinal} csucc(nat){in}T)" using Spec_def
    unfolding IsLindeloef_def by auto
  then have "A{is compact of cardinal} csucc(nat) {in} Pow(A)" using Pow_is_top[of "A"] by auto
  then have "∀M∈Pow(Pow(A)). A⊆⋃M ⟶ (∃N∈Pow(M). A⊆⋃N ∧ N≺csucc(nat))" unfolding IsCompactOfCard_def by auto
  moreover
  have "{{x}. x∈A}∈Pow(Pow(A))" by auto
  moreover
  have "A=⋃{{x}. x∈A}" by auto
  ultimately have "∃N∈Pow({{x}. x∈A}). A⊆⋃N ∧ N≺csucc(nat)" by auto
  then obtain N where "N∈Pow({{x}. x∈A})" "A⊆⋃N" "N≺csucc(nat)" by auto
  then have "N⊆{{x}. x∈A}" "N≺csucc(nat)" "A⊆⋃N" using FinPow_def by auto
  {
    fix t
    assume "t∈{{x}. x∈A}"
    then obtain x where "x∈A""t={x}" by auto
    with ‹A⊆⋃N› have "x∈⋃N" by auto
    then obtain B where "B∈N""x∈B" by auto
    with ‹N⊆{{x}. x∈A}› have "B={x}" by auto
    with ‹t={x}›‹B∈N› have "t∈N" by auto 
  }
  with ‹N⊆{{x}. x∈A}› have "N={{x}. x∈A}" by auto
  let ?B="{⟨x,{x}⟩. x∈A}"
  from ‹N={{x}. x∈A}› have "?B:A→ N" unfolding Pi_def function_def by auto
  with ‹N={{x}. x∈A}› have "?B:inj(A,N)" unfolding inj_def using apply_equality by auto
  then have "A≲N" using lepoll_def by auto
  with ‹N≺csucc(nat)› have "A≺csucc(nat)" using lesspoll_trans1 by auto
  then have "A≲nat" using Card_less_csucc_eq_le Card_nat by auto
  then have "A≺nat∨A≈nat" using lepoll_iff_leqpoll by auto moreover
  {
    assume "A≈nat"
    then have "nat≈A" using eqpoll_sym by auto
    with A have "nat {is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" using equipollent_spect[
      where P="(λT. ((⋃T){is lindeloef in}T))"] by auto
    moreover
    have "Pow(nat){is a topology}" using Pow_is_top by auto
    moreover
    have "⋃Pow(nat)=nat" by auto
    then have "⋃Pow(nat)≈nat" using eqpoll_refl by auto
    ultimately
    have "nat {is compact of cardinal} csucc(nat){in}Pow(nat)" using Spec_def unfolding IsLindeloef_def by auto
    then have "False" using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ[OF InfCard_nat] assms by auto
  }
  ultimately have "A≺nat" by auto
  then show "Finite(A)" using lesspoll_nat_is_Finite by auto
qed

text‹If the axiom of countable choice on subsets of the pow of the natural numbers
doesn't hold, then anti-lindeloef spaces are anti-compact.›

theorem(in topology0) no_choice_imp_anti_lindeloef_is_anti_comp:
  assumes "¬({the axiom of} nat {choice holds for subsets}(Pow(nat)) )" "T{is anti-lindeloef}"
  shows "T{is anti-compact}"
proof-
  have s:"nat≲csucc(nat)" using le_imp_lesspoll[OF Card_csucc[OF Ord_nat]] lt_csucc[OF Ord_nat] le_iff by auto
  {
    fix T assume "T{is a topology}" "(⋃T){is compact in}T"
    then have "(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
    then have "(⋃T){is compact of cardinal}csucc(nat){in}T" using s compact_greater_card Card_csucc[OF Ord_nat] by auto
    then have "(⋃T){is lindeloef in}T" unfolding IsLindeloef_def by auto
  }
  then have "∀T. T{is a topology} ⟶ ((⋃T){is compact in}T) ⟶ ((⋃T){is lindeloef in}T)" by auto
  from eq_spect_rev_imp_anti[OF this] lindeloef_spec2[OF assms(1)] compact_spectrum
    show ?thesis using assms(2) unfolding IsAntiLin_def IsAntiComp_def by auto
qed

text‹If the axiom of countable choice holds for subsets of the power set of the
natural numbers, then there exists a topological space that is anti-lindeloef
but no anti-compact.›

theorem no_choice_imp_anti_lindeloef_is_anti_comp:
  assumes "({the axiom of} nat {choice holds for subsets}(Pow(nat)))"
  shows "({one-point compactification of}Pow(nat)){is anti-lindeloef}"
proof-
  have t:"⋃({one-point compactification of}Pow(nat))={nat}∪nat" using topology0.op_compact_total
    unfolding topology0_def using Pow_is_top by auto
  have "{nat}≈1" using singleton_eqpoll_1 by auto
  then have "{nat}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover
  have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto
  ultimately have "{nat}≺csucc(nat)" using lesspoll_trans by blast
  with s have "{nat}∪nat≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]]
    by auto
  then have "{nat}∪nat≲nat" using Card_less_csucc_eq_le[OF Card_nat] by auto
  with t have r:"⋃({one-point compactification of}Pow(nat))≲nat" by auto
  {
    fix A assume A:"A∈Pow(⋃({one-point compactification of}Pow(nat)))" "(⋃(({one-point compactification of}Pow(nat)){restricted to}A)){is lindeloef in}(({one-point compactification of}Pow(nat)){restricted to}A)"
    from A(1) have "A⊆⋃({one-point compactification of}Pow(nat))" by auto
    with r have "A≲nat" using subset_imp_lepoll lepoll_trans by blast
    then have "A{is in the spectrum of}(λT. ((⋃T){is lindeloef in}T))" using assms
      lindeloef_spec1 by auto
  }
  then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto
qed

theorem op_comp_pow_nat_no_anti_comp:
  shows "¬(({one-point compactification of}Pow(nat)){is anti-compact})"
proof
  let ?T="({one-point compactification of}Pow(nat)){restricted to}({nat} ∪ nat)"
  assume antiComp:"({one-point compactification of}Pow(nat)){is anti-compact}"
  have "({nat} ∪ nat){is compact in}({one-point compactification of}Pow(nat))"
    using topology0.compact_op[of "Pow(nat)"] Pow_is_top[of "nat"] unfolding topology0_def
    by auto
  then have "({nat} ∪ nat){is compact in}?T" using compact_imp_compact_subspace Compact_is_card_nat by auto
  moreover have "⋃?T=(⋃({one-point compactification of}Pow(nat)))∩({nat} ∪ nat)" unfolding RestrictedTo_def by auto
  then have "⋃?T={nat} ∪ nat" using topology0.op_compact_total unfolding topology0_def
    using Pow_is_top by auto
  ultimately have "(⋃?T){is compact in}?T" by auto
  with antiComp have "({nat} ∪ nat){is in the spectrum of}(λT. (⋃T){is compact in}T)" unfolding IsAntiComp_def
    antiProperty_def using topology0.op_compact_total unfolding topology0_def using Pow_is_top by auto
  then have "Finite({nat} ∪ nat)" using compact_spectrum by auto
  then have "Finite(nat)" using subset_Finite by auto
  then show "False" using nat_not_Finite by auto
qed

text‹In coclusion, we reached another equivalence of this choice principle.›

text‹The axiom of countable choice holds for subsets of the power set of the
natural numbers if and only if there exists a topological space which is anti-lindeloef
but not anti-compact; this space can be chosen as the one-point compactification
of the discrete topology on $\mathbb{N}$.›

theorem acc_pow_nat_equiv1:
  shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (({one-point compactification of}Pow(nat)){is anti-lindeloef})"
  using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp
  topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top
  Pow_is_top[of "nat"] unfolding topology0_def by auto

theorem acc_pow_nat_equiv2:
  shows "({the axiom of} nat {choice holds for subsets}(Pow(nat))) ⟷ (∃T. T{is a topology}
  ∧ (T{is anti-lindeloef}) ∧ ¬(T{is anti-compact}))"
  using op_comp_pow_nat_no_anti_comp no_choice_imp_anti_lindeloef_is_anti_comp
  topology0.no_choice_imp_anti_lindeloef_is_anti_comp topology0.op_comp_is_top
  Pow_is_top[of "nat"] unfolding topology0_def by auto

text‹In the file @{file "Topology_ZF_properties.thy"}, it is proven that $\mathbb{N}$ is
lindeloef if and only if the axiom of countable choice holds for subsets of $Pow(\mathbb{N})$.
Now we check that, in ZF, this space is always anti-lindeloef.›

theorem nat_anti_lindeloef:
  shows "Pow(nat){is anti-lindeloef}"
proof-
  {
   fix A assume A:"A∈Pow(⋃Pow(nat))" "(⋃(Pow(nat){restricted to}A)){is lindeloef in}(Pow(nat){restricted to}A)"
    from A(1) have "A⊆nat" by auto
    then have "Pow(nat){restricted to}A=Pow(A)" unfolding RestrictedTo_def by blast
    with A(2) have lin:"A{is lindeloef in}Pow(A)" using subset_imp_lepoll by auto
    {
      fix T assume T:"T{is a topology}" "⋃T≈A"
      then have "A≈⋃T" using eqpoll_sym by auto
      then obtain f where f:"f∈bij(A,⋃T)" unfolding eqpoll_def by auto
      then have "f∈surj(A,⋃T)" unfolding bij_def by auto
      moreover then have "IsContinuous(Pow(A),T,f)" unfolding IsContinuous_def
        surj_def using func1_1_L3 by blast
      moreover have "two_top_spaces0(Pow(A),T,f)" unfolding two_top_spaces0_def
        using f T(1) Pow_is_top unfolding bij_def inj_def by auto
      ultimately have "(⋃T){is lindeloef in}T" using two_top_spaces0.cont_image_com
        lin unfolding IsLindeloef_def by auto
    }
    then have "A{is in the spectrum of} (λT. ((⋃T){is lindeloef in}T))" unfolding Spec_def by auto
  }
  then show ?thesis unfolding IsAntiLin_def antiProperty_def by auto   
qed

text‹This result is interesting because depending on the different axioms we add
to ZF, it means two different things: 
\begin{itemize}
\item Every subspace of $\mathbb{N}$ is Lindeloef.
\item Only the compact subspaces of $\mathbb{N}$ are Lindeloef.
\end{itemize}
›

text‹Now, we could wonder if the class of compact spaces and the class of lindeloef spaces being equal
is consistent in ZF. Let's find a topological space which is lindeloef and no compact
without assuming any axiom of choice or any negation of one. This will prove
that the class of lindeloef spaces and the class of compact spaces cannot be equal
in any model of ZF.›

theorem lord_nat:
  shows "(LOrdTopology nat Le)={LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}"
proof-
  {
    fix U assume U:"U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" "U≠0"
    {
      assume "nat∈U"
      with U have "⋃U=nat" unfolding LeftRayX_def by auto
      then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}∪{0}" by auto
    }
    moreover
    {
      assume "nat∉U"
      with U have UU:"U⊆{LeftRayX(nat,Le,n). n∈nat}∪{0}" by auto
      {
        assume A:"∃i. i∈nat∧ ⋃U⊆ LeftRayX(nat,Le,i)"
        let ?M="μ i. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)"
        from A have M:"?M∈nat" "⋃U⊆ LeftRayX(nat,Le,?M)" using LeastI[OF _ nat_into_Ord, where P="λi. i∈nat ∧ ⋃U⊆ LeftRayX(nat,Le,i)"]
          by auto
        {
          fix y assume V:"y∈LeftRayX(nat,Le,?M)"
          then have y:"y∈nat" unfolding LeftRayX_def by auto
          {
            assume "∀V∈U. y∉V"
            then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. y∉LeftRayX(nat,Le,m)" using UU by auto
            then have "∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨y,m⟩∉Le∨y=m" unfolding LeftRayX_def using y
              by auto
            then have RR:"∀m∈{n∈nat. LeftRayX(nat,Le,n)∈U}. ⟨m,y⟩∈Le" using Le_directs_nat(1) y unfolding IsLinOrder_def IsTotal_def by blast
            {
              fix rr V assume "rr∈⋃U"
              then obtain V where V:"V∈U" "rr∈V" by auto
              with UU obtain m where m:"V=LeftRayX(nat,Le,m)" "m∈nat" by auto
              with V(1) RR have a:"⟨m,y⟩∈Le" by auto
              from V(2) m(1) have b:"⟨rr,m⟩∈Le" "rr∈nat-{m}" unfolding LeftRayX_def by auto
              from a b(1) have "⟨rr,y⟩∈Le" using Le_directs_nat(1) unfolding IsLinOrder_def
                trans_def by blast moreover
              {
                assume "rr=y"
                with a b have "False" using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast
              }
              ultimately have "rr∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using b(2) by auto
            }
            then have "⋃U⊆LeftRayX(nat,Le,y)" by auto
            with y M(1) have "⟨?M,y⟩∈Le" using Least_le by auto
            with V have "False" unfolding LeftRayX_def using Le_directs_nat(1) unfolding IsLinOrder_def antisym_def by blast
          }
          then have "y∈⋃U" by auto
        }
        then have "LeftRayX(nat,Le,?M)⊆⋃U" by auto
        with M(2) have "⋃U=LeftRayX(nat,Le,?M)" by auto
        with M(1) have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat}" by auto
      }
      moreover
      {
        assume "¬(∃i. i ∈ nat ∧ ⋃U ⊆ LeftRayX(nat, Le, i))"
        then have A:"∀i. i∈nat ⟶ ¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto
        {
          fix i assume i:"i∈nat"
          with A have AA:"¬(⋃U ⊆ LeftRayX(nat, Le, i))" by auto
          {
            assume "i∉⋃U"
            then have "∀V∈U. i∉V" by auto
            then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. i∉LeftRayX(nat, Le, m)" by auto
            with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ⟨i,m⟩∉Le∨i=m" unfolding LeftRayX_def by auto
            with i have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. ¬(i≤m)∨i=m" unfolding Le_def by auto
            then have "∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m<i∨m=i" using not_le_iff_lt[OF nat_into_Ord[OF i]
              nat_into_Ord] by auto
            then have M:"∀m∈{n∈nat. LeftRayX(nat, Le, n)∈U}. m≤i" using le_iff nat_into_Ord[OF i] by auto
            {
              fix s assume "s∈⋃U"
              then obtain n where n:"n∈nat" "s∈LeftRayX(nat, Le, n)" "LeftRayX(nat, Le, n)∈U"
                using UU by auto
              with M have ni:"n≤i" by auto
              from n(2) have sn:"s≤n" "s≠n" unfolding LeftRayX_def by auto
              then have "s≤i" "s≠i" using le_trans[OF sn(1) ni] le_anti_sym[OF sn(1)] ni by auto
              then have "s∈LeftRayX(nat, Le, i)" using i le_in_nat unfolding LeftRayX_def by auto
            }
            with AA have "False" by auto
          }
          then have "i∈⋃U" by auto
        }
        then have "nat⊆⋃U" by auto
        then have "⋃U=nat" using UU unfolding LeftRayX_def by auto
        then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
      }
      ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
    }
    ultimately have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
  }
  moreover
  {
    fix U assume "U=0"
    then have "⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}" by auto
  }
  ultimately have "∀U. U⊆{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ⟶ ⋃U∈{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}"
    by auto
  then have "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}={⋃U. U∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat})}" by blast
  then show ?thesis using LOrdtopology_ROrdtopology_are_topologies(2)[OF Le_directs_nat(1)]
    unfolding IsAbaseFor_def by auto
qed

lemma countable_lord_nat:
  shows "{LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}≺csucc(nat)"
proof-
  {
    fix e
    have "{e}≈1" using singleton_eqpoll_1 by auto
    then have "{e}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto moreover
    have s:"nat≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc] lt_csucc[OF Ord_nat] by auto
    ultimately have "{e}≺csucc(nat)" using lesspoll_trans by blast
  }
  then have "{nat} ∪{0}≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat], of "{nat}" "{0}"]
    by auto moreover
  let ?FF="{⟨n,LeftRayX(nat,Le,n)⟩. n∈nat}"
  have ff:"?FF:nat→{LeftRayX(nat,Le,n). n∈nat}" unfolding Pi_def domain_def function_def by auto
  then have su:"?FF∈surj(nat,{LeftRayX(nat,Le,n). n∈nat})" unfolding surj_def using apply_equality[
    OF _ ff] by auto
  then have "{LeftRayX(nat,Le,n). n∈nat}≲nat" using surj_fun_inv_2[OF su lepoll_refl[of "nat"]] Ord_nat 
    by auto
  then have "{LeftRayX(nat,Le,n). n∈nat}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
  ultimately have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0}) ≺ csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]] by auto
  moreover have "{LeftRayX(nat, Le, n) . n ∈ nat} ∪ ({nat} ∪ {0})={LeftRayX(nat, Le, n) . n ∈ nat} ∪ {nat} ∪ {0}" by auto
  ultimately show ?thesis by auto
qed

corollary lindelof_lord_nat:
  shows "nat{is lindeloef in}(LOrdTopology nat Le)"
  unfolding IsLindeloef_def using countable_lord_nat lord_nat card_top_comp[OF Card_csucc[OF Ord_nat]]
    union_lordtopology_rordtopology(1)[OF Le_directs_nat(1)] by auto
  
theorem not_comp_lord_nat:
  shows "¬(nat{is compact in}(LOrdTopology nat Le))"
proof
  assume "nat{is compact in}(LOrdTopology nat Le)"
  with lord_nat have "nat{is compact in}({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0})" by auto
  then have "∀M∈Pow({LeftRayX(nat,Le,n). n∈nat} ∪{nat} ∪{0}). nat⊆⋃M ⟶ (∃N∈FinPow(M). nat⊆⋃N)"
    unfolding IsCompact_def by auto moreover
  {
    fix n assume n:"n∈nat"
    then have "n<succ(n)" by auto
    then have "⟨n,succ(n)⟩∈Le" "n≠succ(n)" using n nat_succ_iff by auto
    then have "n∈LeftRayX(nat,Le,succ(n))" unfolding LeftRayX_def using n by auto
    then have "n∈⋃({LeftRayX(nat,Le,n). n∈nat})" using n nat_succ_iff by auto
  }
  ultimately have "∃N∈FinPow({LeftRayX(nat,Le,n). n∈nat}). nat⊆⋃N" by blast
  then obtain N where "N∈FinPow({LeftRayX(nat,Le,n). n∈nat})" "nat⊆⋃N" by auto
  then have N:"N⊆{LeftRayX(nat,Le,n). n∈nat}" "Finite(N)" "nat⊆⋃N" unfolding FinPow_def by auto
  let ?F="{⟨n,LeftRayX(nat,Le,n)⟩. n∈{m∈nat. LeftRayX(nat,Le,m)∈N}}"
  have ff:"?F:{m∈nat. LeftRayX(nat,Le,m)∈N} → N" unfolding Pi_def function_def by auto
  then have "?F∈surj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding surj_def using N(1) apply_equality[
    OF _ ff] by blast moreover
  {
    fix x y assume xyF:"x∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "y∈{m∈nat. LeftRayX(nat,Le,m)∈N}" "?F`x=?F`y"
    then have "?F`x=LeftRayX(nat,Le,x)" "?F`y=LeftRayX(nat,Le,y)" using apply_equality[
      OF _ ff] by auto
    with xyF(3) have lxy:"LeftRayX(nat,Le,x)=LeftRayX(nat,Le,y)" by auto
    {
      fix r assume "r<x"
      then have "r≤x" "r≠x" using leI by auto
      with xyF(1) have "r∈LeftRayX(nat,Le,x)" unfolding LeftRayX_def using le_in_nat by auto
      then have "r∈LeftRayX(nat,Le,y)" using lxy by auto
      then have "r≤y" "r≠y" unfolding LeftRayX_def by auto
      then have "r<y" using le_iff by auto
    }
    then have "∀r. r<x ⟶ r<y" by auto
    then have r:"¬(y<x)" by auto
    {
      fix r assume "r<y"
      then have "r≤y" "r≠y" using leI by auto
      with xyF(2) have "r∈LeftRayX(nat,Le,y)" unfolding LeftRayX_def using le_in_nat by auto
      then have "r∈LeftRayX(nat,Le,x)" using lxy by auto
      then have "r≤x" "r≠x" unfolding LeftRayX_def by auto
      then have "r<x" using le_iff by auto
    }
    then have "¬(x<y)" by auto
    with r have "x=y" using not_lt_iff_le[OF nat_into_Ord nat_into_Ord] xyF(1,2)
      le_anti_sym by auto
  }
  then have "?F∈inj({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding inj_def using ff by auto
  ultimately have "?F∈bij({m∈nat. LeftRayX(nat,Le,m)∈N}, N)" unfolding bij_def by auto
  then have "{m∈nat. LeftRayX(nat,Le,m)∈N}≈ N" unfolding eqpoll_def by auto
  with N(2) have fin:"Finite({m∈nat. LeftRayX(nat,Le,m)∈N})" using lepoll_Finite eqpoll_imp_lepoll
    by auto
  from N(3) have "N≠0" by auto
  then have nE:"{m∈nat. LeftRayX(nat,Le,m)∈N}≠0" using N(1) by auto
  let ?M="Maximum(Le,{m∈nat. LeftRayX(nat,Le,m)∈N})"
  have M:"?M∈nat" "LeftRayX(nat,Le,?M)∈N" "∀𝔵∈{m∈nat. LeftRayX(nat,Le,m)∈N}. ⟨𝔵,?M⟩∈Le" using fin linord_max_props(1,3)[OF Le_directs_nat(1) _ nE]
    unfolding FinPow_def by auto
  {
    fix V 𝔵 assume V:"V∈N" "𝔵∈V"
    then obtain m where m:"V=LeftRayX(nat,Le,m)" "LeftRayX(nat,Le,m)∈N" "m∈nat" using N(1) by auto
    with V(2) have xx:"⟨𝔵,m⟩∈Le" "𝔵≠m" unfolding LeftRayX_def by auto
    from m(2,3) have "m∈{m∈nat. LeftRayX(nat,Le,m)∈N}" by auto
    then have mM:"⟨m,?M⟩∈Le" using M(3) by auto
    with xx(1) have "⟨𝔵,?M⟩∈Le" using le_trans unfolding Le_def by auto
    moreover
    {
      assume "𝔵=?M"
      with xx mM have "False" using le_anti_sym by auto
    }
    ultimately have "𝔵∈LeftRayX(nat,Le,?M)" unfolding LeftRayX_def by auto
  }
  then have "⋃N⊆LeftRayX(nat,Le,?M)" by auto
  with M(2) have "⋃N=LeftRayX(nat,Le,?M)" by auto
  with N(3) have "nat⊆LeftRayX(nat,Le,?M)" by auto
  moreover from M(1) have "succ(?M)∈nat" using nat_succI by auto
  ultimately have "succ(?M)∈LeftRayX(nat,Le,?M)" by auto
  then have "⟨succ(?M),?M⟩∈Le" unfolding LeftRayX_def by blast
  then show "False" by auto
qed
      
subsection‹More Separation properties›

text‹In this section we study more separation properties.›

subsection‹Definitions›

text‹We start with a property that has already appeared in
@{file "Topology_ZF_1b.thy"}. A KC-space is a space where
compact sets are closed.›

definition
  IsKC ("_ {is KC}") where
  "T{is KC} ≡ ∀A∈Pow(⋃T). A{is compact in}T ⟶ A{is closed in}T"

text‹Another type of space is an US-space; those where sequences
have at most one limit.›

definition
  IsUS ("_{is US}") where
  "T{is US} ≡ ∀N x y. (N:nat→⋃T) ∧ NetConvTop(⟨N,Le⟩,x,T) ∧ NetConvTop(⟨N,Le⟩,y,T) ⟶ y=x"

subsection‹First results›

text‹The proof in @{file "Topology_ZF_1b.thy"} shows that a Hausdorff space
is KC.›

corollary(in topology0) T2_imp_KC:
  assumes "T{is T⇩2}"
  shows "T{is KC}"
proof-
  {
    fix A assume "A{is compact in}T"
    then have "A{is closed in}T" using in_t2_compact_is_cl assms by auto
  }
  then show ?thesis unfolding IsKC_def by auto
qed

text‹From the spectrum of compactness, it follows that any KC-space
is $T_1$.›

lemma(in topology0) KC_imp_T1:
  assumes "T{is KC}"
  shows "T{is T⇩1}"
proof-
  {
    fix x assume A:"x∈⋃T"
    have "Finite({x})" by auto
    then have "{x}{is in the spectrum of}(λT. (⋃T){is compact in}T)"
      using compact_spectrum by auto moreover
    have "(T{restricted to}{x}){is a topology}" using Top_1_L4 by auto
    moreover have "⋃(T{restricted to}{x})={x}" using A unfolding RestrictedTo_def by auto
    ultimately have com:"{x}{is compact in}(T{restricted to}{x})" unfolding Spec_def
      by auto
    then have "{x}{is compact in}T" using compact_subspace_imp_compact A by auto
    then have "{x}{is closed in}T" using assms unfolding IsKC_def using A by auto
  }
  then show ?thesis using T1_iff_singleton_closed by auto
qed

text‹Even more, if a space is KC, then it is US. We already know that
for $T_2$ spaces, any net or filter has at most one limit; and that
this property is equivalent with $T_2$. The US property is much weaker
because we don't know what happends with other nets that are not directed by
the order on the natural numbers.›

theorem(in topology0) KC_imp_US:
  assumes "T{is KC}"
  shows "T{is US}"
proof-
  {
    fix N x y  assume A:"N:nat→⋃T" "⟨N,Le⟩→⇩N x" "⟨N,Le⟩→⇩N y" "x≠y"
    have dir:"Le directs nat" using Le_directs_nat by auto moreover
    from A(1) have dom:"domain(N)=nat" using func1_1_L1 by auto
    moreover note A(1) ultimately have Net:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def
      by auto
    from A(3) have y:"y∈⋃T" unfolding NetConverges_def[OF Net] by auto
    from A(2) have x:"x∈⋃T" unfolding NetConverges_def[OF Net] by auto
    from A(2) have o1:"∀U∈Pow(⋃T). x∈int(U) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" unfolding NetConverges_def[OF Net]
       using dom by auto
    {
      assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y"
      have "{y}{is closed in}T" using y T1_iff_singleton_closed KC_imp_T1 assms by auto
      then have o2:"⋃T-{y}∈T" unfolding IsClosed_def by auto
      then have "int(⋃T-{y})=⋃T-{y}" using Top_2_L3 by auto
      with A(4) x have o3:"x∈int(⋃T-{y})" by auto
      from o2 have "⋃T-{y}∈Pow(⋃T)" by auto
      with o1 o3 obtain r where r:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-{y}" by auto
      from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=y" by auto
      from dir r(1) n(1) obtain z where "⟨r,z⟩∈Le""⟨n,z⟩∈Le""z∈nat" unfolding IsDirectedSet_def by auto
      with r(2) n(2) have "N`z∈⋃T-{y}" "N`z=y" by auto
      then have "False" by auto
    }
    then have reg:"∀n∈nat. ∃m∈nat. N`m≠y ∧ ⟨n,m⟩∈Le" by auto
    let ?NN="{⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩. n∈nat}"
    {
      fix x z assume A1:"⟨x, z⟩ ∈ ?NN"
      {
        fix y' assume A2:"⟨x,y'⟩∈?NN"
        with A1 have "z=y'" by auto
      }
      then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto
    }
    then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto
    moreover
    {
      fix n assume as:"n∈nat"
      with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
      then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"]
        nat_into_Ord[of "m"] by auto
      then have "(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈nat" by auto
      then have "N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)∈⋃T" using apply_type[OF A(1)] by auto
      with as have "⟨n,N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃T" by auto
    }
    then have "?NN∈Pow(nat×⋃T)" by auto
    ultimately have NFun:"?NN:nat→⋃T" unfolding Pi_def function_def domain_def by auto
    {
      fix n assume as:"n∈nat"
      with reg obtain m where "N`m≠y ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
      then have LI:"N`(μ i. N`i≠y ∧ ⟨n,i⟩∈Le)≠y" "⟨n,μ i. N`i≠y ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨n,m⟩∈Le" "m"]
        nat_into_Ord[of "m"] by auto
      then have "?NN`n≠y" using apply_equality[OF _ NFun] by auto
    }
    then have noy:"∀n∈nat. ?NN`n≠y" by auto
    have dom2:"domain(?NN)=nat" by auto
    then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using NFun dir by auto
    {
      fix U assume "U∈Pow(⋃T)" "x∈int(U)"
      then have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" using o1 by auto
      then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" by auto
      {
        fix s assume AA:"⟨r,s⟩∈Le"
        with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto
        then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"]
          nat_into_Ord by auto
        with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
        with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈U" by blast
        then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
      }
      then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
      with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
    }
    then have conv2:"⟨?NN,Le⟩→⇩N x" unfolding NetConverges_def[OF net2] using x dom2 by auto
    let ?A="{x}∪?NN``nat"
    {
      fix M assume Acov:"?A⊆⋃M" "M⊆T"
      then have "x∈⋃M" by auto
      then obtain U where U:"x∈U" "U∈M" by auto
      with Acov(2) have UT:"U∈T" by auto
      then have "U=int(U)" using Top_2_L3 by auto
      with U(1) have "x∈int(U)" by auto
      with conv2 obtain r where rr:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U"
        unfolding NetConverges_def[OF net2] using dom2 UT by auto
      have NresFun:"restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}):{n∈nat. ⟨n,r⟩∈Le}→⋃T" using restrict_fun
        [OF NFun, of "{n∈nat. ⟨n,r⟩∈Le}"] by auto
      then have "restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})∈surj({n∈nat. ⟨n,r⟩∈Le},range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})))"
        using fun_is_surj by auto moreover
      have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
      then have "{n∈nat. ⟨n,r⟩∈Le}≲nat" using subset_imp_lepoll by auto
      ultimately have "range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}))≲{n∈nat. ⟨n,r⟩∈Le}" using surj_fun_inv_2 by auto
      moreover
      have "{n∈nat. ⟨n,0⟩∈Le}={0}" by auto
      then have "Finite({n∈nat. ⟨n,0⟩∈Le})" by auto moreover
      {
        fix j assume as:"j∈nat" "Finite({n∈nat. ⟨n,j⟩∈Le})"
        {
          fix t assume "t∈{n∈nat. ⟨n,succ(j)⟩∈Le}"
          then have "t∈nat" "⟨t,succ(j)⟩∈Le" by auto
          then have "t≤succ(j)" by auto
          then have "t⊆succ(j)" using le_imp_subset by auto
          then have "t⊆j ∪{j}" using succ_explained by auto
          then have "j∈t∨t⊆j" by auto
          then have "j∈t∨t≤j" using subset_imp_le ‹t∈nat› ‹j∈nat› nat_into_Ord by auto
          then have "j ∪{j}⊆t∨t≤j" using ‹t∈nat› ‹j∈nat› nat_into_Ord unfolding Ord_def
            Transset_def by auto
          then have "succ(j)⊆t∨t≤j" using succ_explained by auto
          with ‹t⊆succ(j)› have "t=succ(j)∨t≤j" by auto
          with ‹t∈nat› ‹j∈nat› have "t∈{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
        }
        then have "{n∈nat. ⟨n,succ(j)⟩∈Le} ⊆{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
        moreover have "Finite({n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)})" using as(2) Finite_cons
          by auto
        ultimately have "Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" using subset_Finite by auto
      }
      then have "∀j∈nat. Finite({n∈nat. ⟨n,j⟩∈Le}) ⟶ Finite({n∈nat. ⟨n,succ(j)⟩∈Le})"
        by auto
      ultimately have "Finite(range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le})))"
        using lepoll_Finite[of "range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))"
          "{n ∈ nat . ⟨n, r⟩ ∈ Le}"] ind_on_nat[OF ‹r∈nat›, where P="λt. Finite({n∈nat. ⟨n,t⟩∈Le})"] by auto
      then have "Finite((restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using range_image_domain[OF NresFun]
        by auto
      then have "Finite(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using restrict_image by auto
      then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
      moreover have "⋃(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})=⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
        unfolding RestrictedTo_def by auto moreover
      have "⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}=?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
        using func1_1_L6(2)[OF NFun] by blast
      moreover have "(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is a topology}"
        using Top_1_L4 by auto
      ultimately have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})"
        unfolding Spec_def by force
      then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}T" using compact_subspace_imp_compact by auto
      moreover from Acov(1) have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃M" by auto
      moreover note Acov(2) ultimately
      obtain 𝔑 where 𝔑:"𝔑∈FinPow(M)" "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃𝔑"
        unfolding IsCompact_def by blast
      from 𝔑(1) have "𝔑 ∪{U}∈FinPow(M)" using U(2) unfolding FinPow_def by auto moreover
      {
        fix s assume s:"s∈?A" "s∉U"
        with U(1) have "s∈?NN``nat" by auto
        then have "s∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
        then obtain n where n:"n∈nat" "s=?NN`n" by auto
        {
          assume "⟨r,n⟩∈Le"
          with rr have "?NN`n∈U" by auto
          with n(2) s(2) have "False" by auto
        }
        then have "⟨r,n⟩∉Le" by auto
        with rr(1) n(1) have "¬(r≤n)" by auto
        then have "n≤r" using Ord_linear_le[where thesis="⟨n,r⟩∈Le"] nat_into_Ord[OF rr(1)]
          nat_into_Ord[OF n(1)] by auto
        with rr(1) n(1) have "⟨n,r⟩∈Le" by auto
        with n(2) have "s∈{?NN`t. t∈{n∈nat. ⟨n,r⟩∈Le}}" by auto moreover
        have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
        ultimately have "s∈?NN``{n∈nat. ⟨n,r⟩∈Le}" using func_imagedef[OF NFun]
          by auto
        with 𝔑(2) have "s∈⋃𝔑" by auto
      }
      then have "?A⊆⋃𝔑 ∪ U" by auto
      then have "?A⊆⋃(𝔑 ∪ {U})" by auto ultimately
      have "∃𝔑∈FinPow(M). ?A⊆⋃𝔑" by auto
    }
    then have "∀M∈Pow(T). ?A⊆⋃M ⟶ (∃𝔑∈FinPow(M). ?A⊆⋃𝔑)" by auto moreover
    have "?A⊆⋃T" using func1_1_L6(2)[OF NFun] x by blast ultimately
    have "?A{is compact in}T" unfolding IsCompact_def by auto
    with assms have "?A{is closed in}T" unfolding IsKC_def IsCompact_def by auto
    then have "⋃T-?A∈T" unfolding IsClosed_def by auto
    then have "⋃T-?A=int(⋃T-?A)" using Top_2_L3 by auto moreover
    {
      assume "y∈?A"
      with A(4) have "y∈?NN``nat" by auto
      then have "y∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
      then obtain n where "n∈nat""?NN`n=y" by auto
      with noy have "False" by auto
    }
    with y have "y∈⋃T-?A" by force ultimately
    have "y∈int(⋃T-?A)" "⋃T-?A∈Pow(⋃T)" by auto moreover
    have "(∀U∈Pow(⋃T).  y ∈ int(U) ⟶ (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U))"
      using A(3) dom unfolding NetConverges_def[OF Net] by auto
    ultimately have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T-?A" by blast
    then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈⋃T-?A" by auto
    {
        fix s assume AA:"⟨r,s⟩∈Le"
        with reg obtain m where "N`m≠y" "⟨s,m⟩∈Le" by auto
        then have "⟨s,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠y ∧ ⟨s,m⟩∈Le" "m"]
          nat_into_Ord by auto
        with AA have "⟨r,μ i. N`i≠y ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
        with r_def(2) have "N`(μ i. N`i≠y ∧ ⟨s,i⟩∈Le)∈⋃T-?A" by force
        then have "?NN`s∈⋃T-?A" using apply_equality[OF _ NFun] AA by auto
        moreover have "?NN`s∈{?NN`t. t∈nat}" using AA by auto
        then have "?NN`s∈?NN``nat" using func_imagedef[OF NFun] by auto
        then have "?NN`s∈?A" by auto
        ultimately have "False" by auto
      }
      moreover have "r⊆succ(r)" using succ_explained by auto
      then have "r≤succ(r)" using subset_imp_le nat_into_Ord ‹r∈nat› nat_succI
        by auto
      then have "⟨r,succ(r)⟩∈Le" using ‹r∈nat› nat_succI by auto
      ultimately have "False" by auto
    }
    then have "∀N x y. (N:nat→⋃T) ∧ (⟨N, Le⟩ →⇩N x {in} T) ∧ (⟨N, Le⟩ →⇩N y {in} T)
      ⟶ x=y" by auto
  then show ?thesis unfolding IsUS_def by auto
qed

text‹US spaces are also $T_1$.›

theorem (in topology0) US_imp_T1:
  assumes "T{is US}"
  shows "T{is T⇩1}"
proof-
  {
    fix x assume x:"x∈⋃T"
    then have "{x}⊆⋃T" by auto
    {
      fix y assume y:"y≠x" "y∈cl({x})"
      then have r:"∀U∈T. y∈U ⟶ x∈U" using cl_inter_neigh[OF ‹{x}⊆⋃T›] by auto
      let ?N="ConstantFunction(nat,x)"
      have fun:"?N:nat→⋃T" using x func1_3_L1 by auto
      then have dom:"domain(?N)=nat" using func1_1_L1 by auto
      with fun have Net:"⟨?N,Le⟩{is a net on}⋃T" using Le_directs_nat unfolding IsNet_def
        by auto
      {
        fix U assume "U∈Pow(⋃T)" "x∈int(U)"
        then have "x∈U" using Top_2_L1 by auto
        then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto
        then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto
        then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto
      }
      then have "⟨?N,Le⟩ →⇩N x" unfolding NetConverges_def[OF Net] using x dom by auto moreover
      {
        fix U assume "U∈Pow(⋃T)" "y∈int(U)"
        then have "x∈int(U)" using r Top_2_L2 by auto
        then have "x∈U" using Top_2_L1 by auto
        then have "∀n∈nat. ?N`n∈U" using func1_3_L2 by auto
        then have "∀n∈nat. ⟨0,n⟩∈Le ⟶?N`n∈U" by auto
        then have "∃r∈nat. ∀n∈nat. ⟨r,n⟩∈Le ⟶?N`n∈U" by auto
      }
      then have "⟨?N,Le⟩ →⇩N y" unfolding NetConverges_def[OF Net] using y(2) dom
        Top_3_L11(1)[OF ‹{x}⊆⋃T›] by auto
      ultimately have "x=y" using assms unfolding IsUS_def using fun by auto
      with y(1) have "False" by auto
    }
    then have "cl({x})⊆{x}" by auto
    then have "cl({x})={x}" using cl_contains_set[OF ‹{x}⊆⋃T›] by auto
    then have "{x}{is closed in}T" using Top_3_L8 x by auto
  }
  then show ?thesis using T1_iff_singleton_closed by auto
qed

subsection‹Counter-examples›

text‹We need to find counter-examples that prove that this properties
are new ones.›

text‹We know that $T_2\Rightarrow loc.T_2\Rightarrow$ anti-hyperconnected $\Rightarrow T_1$
and $T_2\Rightarrow KC\Rightarrow US\Rightarrow T_1$. The question is: What is the relation
between $KC$ or $US$ and, $loc.T_2$ or anti-hyperconnected?›

text‹In the file @{file "Topology_ZF_properties_2.thy"} we built a topological space
which is locally-$T_2$ but no $T_2$. It happends actually that this space is not even US
given the appropiate topology ‹T›.›

lemma (in topology0) locT2_not_US_1:
  assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩N m) ∧ m∉N``nat" 
  shows "∃N∈nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). (⟨N,Le⟩→⇩N ⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))
    ∧ (⟨N,Le⟩→⇩N m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))"
proof-
  from assms(3) obtain N where N:"N:nat→⋃T" "⟨N,Le⟩→⇩N m" "m∉N``nat" by auto
  have "⋃T⊆⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top
    by auto
  with N(1) have fun:"N:nat→⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using func1_1_L1B by auto
  then have dom:"domain(N)=nat" using func1_1_L1 by auto
  with fun have Net:"⟨N,Le⟩{is a net on}⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" unfolding
    IsNet_def using Le_directs_nat by auto
  from N(1) dom have Net2:"⟨N,Le⟩{is a net on}⋃T" unfolding IsNet_def using Le_directs_nat by auto
  from N(2) have R:"∀U∈Pow(⋃T). m∈int(U) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)"
    unfolding NetConverges_def[OF Net2] using dom by auto
  {
    fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))"  "m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast
    then have "(⋃T)∩?I∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" unfolding RestrictedTo_def by blast
    then have "(⋃T)∩?I∈T" using open_subspace_double_point(1) assms(2) by auto moreover
    then have "int((⋃T)∩?I)=(⋃T)∩?I" using Top_2_L3 by auto
    with U(2) assms(2) have "m∈int((⋃T)∩?I)" unfolding IsClosed_def by auto
    moreover note R ultimately have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈(⋃T)∩?I" by blast
    then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" by blast
    then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1[of "T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}""U"] doble_point_top assms(2)
      unfolding topology0_def by auto
  }
  then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). m∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto
  moreover have tt:"topology0(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using doble_point_top[OF assms(2)] unfolding topology0_def. 
  have "m∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top unfolding IsClosed_def by auto ultimately
  have con1:"(⟨N,Le⟩→⇩N m {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net]
    using dom by auto
  {
    fix U assume U:"U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))"  "⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    let ?I="Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    have "?I∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using topology0.Top_2_L2 assms(2) doble_point_top unfolding topology0_def by blast
    with U(2) mem_not_refl have "?I∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
    then obtain V W where VW:"?I=(V-{m})∪{⋃T}∪W" "W∈T" "V∈T" "m∈V" by auto
    from VW(3,4) have "m∈int(V)" using Top_2_L3 by auto moreover
    have "V∈Pow(⋃T)" using VW(3) by auto moreover
    note R ultimately
    have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V" by blast moreover
    from N(3) have "∀s∈nat. N`s≠m" using func_imagedef[OF N(1)] by auto ultimately
    have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈V-{m}" by blast
    then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈?I" using VW(1) by auto
    then have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using topology0.Top_2_L1 assms(2) doble_point_top unfolding topology0_def by blast
  }
  then have "∀U∈Pow(⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})). ⋃T∈Interior(U,T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) ⟶ (∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U)" by auto
  moreover have "⋃T∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using assms(2) union_doublepoint_top by auto ultimately
  have "(⟨N,Le⟩→⇩N ⋃T {in} (T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))" unfolding topology0.NetConverges_def[OF tt Net]
    using dom by auto
  with con1 fun show ?thesis by auto
qed

corollary (in topology0) locT2_not_US_2:
  assumes "{m}∉T" "{m}{is closed in}T" "∃N∈nat→⋃T. (⟨N,Le⟩→⇩N m) ∧ m∉N``nat"
  shows "¬((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){is US})"
proof-
  have "m≠⋃T" using assms(2) mem_not_refl unfolding IsClosed_def by auto 
  then show ?thesis using locT2_not_US_1 assms unfolding IsUS_def by blast
qed

text‹In particular, we also know that a locally-$T_2$ space doesn't need to be KC;
since KC$\Rightarrow$US. Also we know that anti-hyperconnected spaces don't need to be
KC or US, since locally-$T_2\Rightarrow$anti-hyperconnected.›

text‹Let's find a KC space that is not $T_2$, an US space which is not KC
and a $T_1$ space which is not US.›

text‹First, let's prove some lemmas about what relation
is there between this properties under the influence of other ones. This will
help us to find counter-examples.›

text‹Anti-compactness ereases the differences between several properties.›

lemma (in topology0) anticompact_KC_equiv_T1:
  assumes "T{is anti-compact}"
  shows "T{is KC}⟷T{is T⇩1}"
proof
  assume "T{is KC}"
  then show "T{is T⇩1}" using KC_imp_T1 by auto
next
  assume AS:"T{is T⇩1}"
  {
    fix A assume A:"A{is compact in}T" "A∈Pow(⋃T)"
    then have "A{is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" using compact_imp_compact_subspace
      Compact_is_card_nat by auto
    moreover then have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
    ultimately have "(⋃(T{restricted to}A)){is compact in}(T{restricted to}A)" "A∈Pow(⋃T)" by auto
    with assms have "Finite(A)" unfolding IsAntiComp_def antiProperty_def using compact_spectrum by auto
    then obtain n where "n∈nat" "A≈n" unfolding Finite_def by auto
    then have "A≺nat" using eq_lesspoll_trans n_lesspoll_nat by auto moreover
    have "⋃T-(⋃T-A)=A" using A(2) by auto
    ultimately have "⋃T-(⋃T-A)≺nat" by auto
    then have "⋃T-A∈CoFinite ⋃T" unfolding Cofinite_def CoCardinal_def by auto
    then have "⋃T-A∈T" using AS T1_cocardinal_coarser by auto
    with A(2) have "A{is closed in}T" unfolding IsClosed_def by auto
  }
  then show "T{is KC}" unfolding IsKC_def by auto
qed

text‹Then if we find an anti-compact and $T_1$ but no $T_2$ space,
there is a counter-example for $KC\Rightarrow T_2$. A counter-example for US doesn't
need to be KC mustn't be anti-compact.›

text‹The cocountable topology on ‹csucc(nat)› is such a topology.›
text‹The cocountable topology on $\mathbb{N}^+$ is hyperconnected.›

lemma cocountable_in_csucc_nat_HConn:
  shows "(CoCountable csucc(nat)){is hyperconnected}"
proof-
  {
    fix U V assume as:"U∈(CoCountable csucc(nat))""V∈(CoCountable csucc(nat))""U∩V=0"
    then have "csucc(nat)-U≺csucc(nat)∨U=0""csucc(nat)-V≺csucc(nat)∨V=0"
      unfolding Cocountable_def CoCardinal_def by auto
    then have "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)∨U=0∨V=0" using less_less_imp_un_less[
      OF _ _ InfCard_csucc[OF InfCard_nat]] by auto moreover
    {
      assume "(csucc(nat)-U)∪(csucc(nat)-V)≺csucc(nat)" moreover
      have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)-U∩V" by auto
      with as(3) have "(csucc(nat)-U)∪(csucc(nat)-V)=csucc(nat)" by auto
      ultimately have "csucc(nat)≺csucc(nat)" by auto
      then have "False" by auto
    }
    ultimately have "U=0∨V=0" by auto
  }
  then show "(CoCountable csucc(nat)){is hyperconnected}" unfolding IsHConnected_def by auto
qed

text‹The cocountable topology on $\mathbb{N}^+$ is not anti-hyperconnected.›

corollary cocountable_in_csucc_nat_notAntiHConn:
  shows "¬((CoCountable csucc(nat)){is anti-}IsHConnected)"
proof
  assume as:"(CoCountable csucc(nat)){is anti-}IsHConnected"
  have "(CoCountable csucc(nat)){is hyperconnected}" using cocountable_in_csucc_nat_HConn by auto moreover
  have "csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto
  then have uni:"⋃(CoCountable csucc(nat))=csucc(nat)" using union_cocardinal unfolding Cocountable_def by auto
  have "∀A∈(CoCountable csucc(nat)). A⊆⋃(CoCountable csucc(nat))" by fast
  with uni have "∀A∈(CoCountable csucc(nat)). A⊆csucc(nat)" by auto
  then have "∀A∈(CoCountable csucc(nat)). csucc(nat)∩A=A" by auto
  ultimately have "((CoCountable csucc(nat)){restricted to}csucc(nat)){is hyperconnected}"
    unfolding RestrictedTo_def by auto
  with as have "(csucc(nat)){is in the spectrum of}IsHConnected" unfolding antiProperty_def
    using uni by auto
  then have "csucc(nat)≲1" using HConn_spectrum by auto
  then have "csucc(nat)≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
  then show "False" using lt_csucc[OF Ord_nat] lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]]
    lesspoll_trans by auto
qed

text‹The cocountable topology on $\mathbb{N}^+$ is not $T_2$.›

theorem cocountable_in_csucc_nat_noT2:
  shows "¬(CoCountable csucc(nat)){is T⇩2}"
proof
  assume "(CoCountable csucc(nat)){is T⇩2}" 
  then have antiHC:"(CoCountable csucc(nat)){is anti-}IsHConnected" 
    using topology0.T2_imp_anti_HConn[OF topology0_CoCardinal[OF InfCard_csucc[OF InfCard_nat]]]
    unfolding Cocountable_def by auto
  then show "False" using cocountable_in_csucc_nat_notAntiHConn by auto
qed
    
text‹The cocountable topology on $\mathbb{N}^+$ is $T_1$.›

theorem cocountable_in_csucc_nat_T1:
  shows "(CoCountable csucc(nat)){is T⇩1}"
  using cocardinal_is_T1[OF InfCard_csucc[OF InfCard_nat]] unfolding Cocountable_def by auto
    
text‹The cocountable topology on $\mathbb{N}^+$ is anti-compact.›

theorem cocountable_in_csucc_nat_antiCompact:
  shows "(CoCountable csucc(nat)){is anti-compact}"
proof-
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto 
  {
    fix A assume as:"A⊆⋃(CoCountable csucc(nat))" "(⋃((CoCountable csucc(nat)){restricted to}A)){is compact in}((CoCountable csucc(nat)){restricted to}A)"
    from as(1) have ass:"A⊆csucc(nat)" using union_cocardinal[OF noE] unfolding Cocountable_def by auto
    have "((CoCountable csucc(nat)){restricted to}A)=CoCountable (A∩csucc(nat))" using subspace_cocardinal
      unfolding Cocountable_def by auto moreover
    from ass have "A∩csucc(nat)=A" by auto
    ultimately have "((CoCountable csucc(nat)){restricted to}A)=CoCountable A" by auto
    with as(2) have comp:"(⋃(CoCountable A)){is compact in}(CoCountable A)" by auto   
    {
      assume as2:"A≺csucc(nat)" moreover
      {
        fix t assume t:"t∈A"
        have "A-{t}⊆A" by auto
        then have "A-{t}≲A" using subset_imp_lepoll by auto
        with as2 have "A-{t}≺csucc(nat)" using lesspoll_trans1 by auto moreover note noE
        ultimately have "(A-{t}){is closed in}(CoCountable A)" using closed_sets_cocardinal[of "csucc(nat)"
          "A-{t}""A"] unfolding Cocountable_def by auto
        then have "A-(A-{t})∈(CoCountable A)" unfolding IsClosed_def using union_cocardinal[OF noE, of "A"]
          unfolding Cocountable_def by auto moreover
        from t have "A-(A-{t})={t}" by auto ultimately
        have "{t}∈(CoCountable A)" by auto
      }
      then have r:"∀t∈A. {t}∈(CoCountable A)" by auto
      {
        fix U assume U:"U∈Pow(A)"
        {
          fix t assume "t∈U"
          with U r have "t∈{t}""{t}⊆U""{t}∈(CoCountable A)" by auto
          then have "∃V∈(CoCountable A). t∈V ∧ V⊆U" by auto
        }
        then have "U∈(CoCountable A)" using topology0.open_neigh_open[OF topology0_CoCardinal[
          OF InfCard_csucc[OF InfCard_nat]]] unfolding Cocountable_def by auto
      }
      then have "Pow(A)⊆(CoCountable A)" by auto moreover
      {
        fix B assume "B∈(CoCountable A)"
        then have "B∈Pow(⋃(CoCountable A))" by auto
        then have "B∈Pow(A)" using union_cocardinal[OF noE] unfolding Cocountable_def by auto
      }
      ultimately have p:"Pow(A)=(CoCountable A)" by auto
      then have "(CoCountable A){is anti-compact}" using pow_anti_compact[of "A"] by auto moreover
      from p have "⋃(CoCountable A)=⋃Pow(A)" by auto
      then have tot:"⋃(CoCountable A)=A" by auto
      from comp have "(⋃((CoCountable A){restricted to}(⋃(CoCountable A)))){is compact in}((CoCountable A){restricted to}(⋃(CoCountable A)))" using compact_imp_compact_subspace
        Compact_is_card_nat tot unfolding RestrictedTo_def by auto
      ultimately have "A{is in the spectrum of}(λT. (⋃T){is compact in}T)"
        using comp tot unfolding IsAntiComp_def antiProperty_def by auto
    }
    moreover
    {
      assume as1:"¬(A≺csucc(nat))"
      from ass have "A≲csucc(nat)" using subset_imp_lepoll by auto
      with as1 have "A≈csucc(nat)" using lepoll_iff_leqpoll by auto
      then have "csucc(nat)≈A" using eqpoll_sym by auto
      then have "nat≺A" using lesspoll_eq_trans lt_csucc[OF Ord_nat]
        lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]] by auto
      then have "nat≲A" using lepoll_iff_leqpoll by auto
      then obtain f where "f∈inj(nat,A)" unfolding lepoll_def by auto moreover
      then have fun:"f:nat→A" unfolding inj_def by auto
      then have "f∈surj(nat,range(f))" using fun_is_surj by auto
      ultimately have "f∈bij(nat,range(f))" unfolding bij_def inj_def surj_def by auto
      then have "nat≈range(f)" unfolding eqpoll_def by auto
      then have e:"range(f)≈nat" using eqpoll_sym by auto
      then have as2:"range(f)≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]]
        lt_csucc[OF Ord_nat] eq_lesspoll_trans by auto
      then have "range(f){is closed in}(CoCountable A)" using closed_sets_cocardinal[of "csucc(nat)"
          "range(f)""A"] unfolding Cocountable_def using func1_1_L5B[OF fun] noE by auto
      then have "(A∩range(f)){is compact in}(CoCountable A)" using compact_closed union_cocardinal[OF noE, of "A"]
        comp Compact_is_card_nat unfolding Cocountable_def by auto
      moreover have int:"A∩range(f)=range(f)""range(f)∩A=range(f)" using func1_1_L5B[OF fun] by auto
      ultimately have "range(f){is compact in}(CoCountable A)" by auto
      then have "range(f){is compact in}((CoCountable A){restricted to}range(f))" using compact_imp_compact_subspace
        Compact_is_card_nat by auto
      moreover have "((CoCountable A){restricted to}range(f))=CoCountable (range(f)∩A)"
        using subspace_cocardinal unfolding Cocountable_def by auto
      with int(2) have "((CoCountable A){restricted to}range(f))=CoCountable range(f)" by auto
      ultimately have comp2:"range(f){is compact in}(CoCountable range(f))" by auto
      {
        fix t assume t:"t∈range(f)"
        have "range(f)-{t}⊆range(f)" by auto
        then have "range(f)-{t}≲range(f)" using subset_imp_lepoll by auto
        with as2 have "range(f)-{t}≺csucc(nat)" using lesspoll_trans1 by auto moreover note noE
        ultimately have "(range(f)-{t}){is closed in}(CoCountable range(f))" using closed_sets_cocardinal[of "csucc(nat)"
          "range(f)-{t}""range(f)"] unfolding Cocountable_def by auto
        then have "range(f)-(range(f)-{t})∈(CoCountable range(f))" unfolding IsClosed_def using union_cocardinal[OF noE, of "range(f)"]
          unfolding Cocountable_def by auto moreover
        from t have "range(f)-(range(f)-{t})={t}" by auto ultimately
        have "{t}∈(CoCountable range(f))" by auto
      }
      then have r:"∀t∈range(f). {t}∈(CoCountable range(f))" by auto
      {
        fix U assume U:"U∈Pow(range(f))"
        {
          fix t assume "t∈U"
          with U r have "t∈{t}""{t}⊆U""{t}∈(CoCountable range(f))" by auto
          then have "∃V∈(CoCountable range(f)). t∈V ∧ V⊆U" by auto
        }
        then have "U∈(CoCountable range(f))" using topology0.open_neigh_open[OF topology0_CoCardinal[
          OF InfCard_csucc[OF InfCard_nat]]] unfolding Cocountable_def by auto
      }
      then have "Pow(range(f))⊆(CoCountable range(f))" by auto moreover
      {
        fix B assume "B∈(CoCountable range(f))"
        then have "B∈Pow(⋃(CoCountable range(f)))" by auto
        then have "B∈Pow(range(f))" using union_cocardinal[OF noE] unfolding Cocountable_def by auto
      }
      ultimately have p:"Pow(range(f))=(CoCountable range(f))" by blast
      then have "(CoCountable range(f)){is anti-compact}" using pow_anti_compact[of "range(f)"] by auto moreover
      from p have "⋃(CoCountable range(f))=⋃Pow(range(f))" by auto
      then have tot:"⋃(CoCountable range(f))=range(f)" by auto
      from comp2 have "(⋃((CoCountable range(f)){restricted to}(⋃(CoCountable range(f))))){is compact in}((CoCountable range(f)){restricted to}(⋃(CoCountable range(f))))" using compact_imp_compact_subspace
        Compact_is_card_nat tot unfolding RestrictedTo_def by auto
      ultimately have "range(f){is in the spectrum of}(λT. (⋃T){is compact in}T)"
        using comp tot unfolding IsAntiComp_def antiProperty_def by auto
      then have "Finite(range(f))" using compact_spectrum by auto
      then have "Finite(nat)" using e eqpoll_imp_Finite_iff by auto
      then have "False" using nat_not_Finite by auto
    }
    ultimately have "A{is in the spectrum of}(λT. (⋃T){is compact in}T)" by auto
  }
  then have "∀A∈Pow(⋃(CoCountable csucc(nat))). ((⋃((CoCountable csucc(nat)) {restricted to} A)) {is compact in} ((CoCountable csucc(nat)) {restricted to} A))
    ⟶ (A{is in the spectrum of}(λT. (⋃T){is compact in}T))" by auto
  then show ?thesis unfolding IsAntiComp_def antiProperty_def by auto
qed

text‹In conclusion, the cocountable topology defined on ‹csucc(nat)›
is KC but not $T_2$. Also note that is KC but not anti-hyperconnected, hence KC or US
spaces need not to be sober.›

text‹The cofinite topology on the natural numbers is $T_1$, but
not US.›

theorem cofinite_not_US:
  shows "¬((CoFinite nat){is US})"
proof
  assume A:"(CoFinite nat){is US}"
  let ?N="id(nat)"
  have f:"?N:nat→nat" using id_type by auto
  then have fun:"?N:nat→⋃(CoCardinal(nat,nat))" using union_cocardinal unfolding Cofinite_def by auto
  then have dom:"domain(?N)=nat" using func1_1_L1 by auto
  with fun have NET:"⟨?N,Le⟩{is a net on}⋃(CoCardinal(nat,nat))" unfolding IsNet_def
    using Le_directs_nat by auto
  have tot:"⋃(CoCardinal(nat,nat))=nat" using union_cocardinal by auto
  {
    fix U n assume U:"U∈Pow(⋃(CoFinite nat))" "n∈Interior(U,(CoFinite nat))"
    have "Interior(U,(CoFinite nat))∈(CoFinite nat)" using topology0.Top_2_L2
      topology0_CoCardinal[OF InfCard_nat] unfolding Cofinite_def by auto
    then have "nat-Interior(U,(CoFinite nat))≺nat" using U(2) unfolding Cofinite_def
      CoCardinal_def by auto
    then have "Finite(nat-Interior(U,(CoFinite nat)))" using lesspoll_nat_is_Finite by auto moreover
    have "nat-U⊆nat-Interior(U,(CoFinite nat))" using topology0.Top_2_L1
      topology0_CoCardinal[OF InfCard_nat] unfolding Cofinite_def by auto
    ultimately have fin:"Finite(nat-U)" using subset_Finite by auto
    moreover have lin:"IsLinOrder(nat,Le)" using Le_directs_nat(1) by auto
    then have "IsLinOrder(nat-U,Le)" using ord_linear_subset[of "nat" "Le" "nat-U"] by auto
    ultimately have r:"nat-U=0 ∨ (∀r∈nat-U. ⟨r,Maximum(Le,nat-U)⟩∈Le)" using linord_max_props(3)[of "nat-U""Le""nat-U"]
      unfolding FinPow_def by auto
    {
      assume reg:"∀s∈nat. ∃r∈nat. ⟨s,r⟩∈Le ∧ ?N`r∉U"
      with r have s:"(∀r∈nat-U. ⟨r,Maximum(Le,nat-U)⟩∈Le)" "nat-U≠0" using apply_type[OF f] by auto
      have "Maximum(Le,nat-U)∈nat" using linord_max_props(2)[OF lin _ s(2)] fin
        unfolding FinPow_def by auto
      then have "succ(Maximum(Le,nat-U))∈nat" using nat_succI by auto
      with reg have "∃r∈nat. ⟨succ(Maximum(Le,nat-U)),r⟩∈Le ∧ ?N`r∉U" by auto
      then obtain r where r_def:"r∈nat" "⟨succ(Maximum(Le,nat-U)),r⟩∈Le" "?N`r∉U" by auto
      from r_def(1,3) have "?N`r∈nat-U" using apply_type[OF f] by auto
      with s(1) have "⟨?N`r,Maximum(Le,nat-U)⟩∈Le" by auto
      then have "⟨r,Maximum(Le,nat-U)⟩∈Le" using id_conv r_def(1) by auto
      then have "r<succ(Maximum(Le,nat-U))" by auto
      with r_def(2) have "r<r" using lt_trans2 by auto
      then have "False" by auto
    }
    then have "∃s∈nat. ∀r∈nat. ⟨s,r⟩∈Le ⟶ ?N`r∈U" by auto
  }
  then have "∀n∈nat. ∀U∈Pow(⋃(CoFinite nat)). n∈Interior(U,CoFinite nat) ⟶ (∃s∈nat. ∀r∈nat. ⟨s,r⟩∈Le ⟶ ?N`r∈U)" by auto
  with tot have "∀n∈⋃(CoCardinal(nat,nat)). ∀U∈Pow(⋃(CoCardinal(nat,nat))). n∈Interior(U,CoCardinal(nat,nat)) ⟶ (∃s∈nat. ∀r∈nat. ⟨s,r⟩∈Le ⟶ ?N`r∈U)"
    unfolding Cofinite_def by auto
  then have "∀n∈⋃(CoCardinal(nat,nat)). (⟨?N,Le⟩→⇩N n {in}(CoCardinal(nat,nat)))" unfolding topology0.NetConverges_def[OF topology0_CoCardinal[OF InfCard_nat] NET]
    using dom by auto
  with tot have "∀n∈nat. (⟨?N,Le⟩→⇩N n {in}(CoFinite nat))" unfolding Cofinite_def by auto
  then have "(⟨?N,Le⟩→⇩N 0 {in}(CoFinite nat)) ∧ (⟨?N,Le⟩→⇩N 1 {in}(CoFinite nat)) ∧ 0≠1" by auto
  then show "False" using A unfolding IsUS_def using fun unfolding Cofinite_def by auto
qed

text‹To end, we need a space which is US but no KC. This example
comes from the one point compactification of a $T_2$, anti-compact
and non discrete space. This $T_2$, anti-compact and non discrete space
comes from a construction over the cardinal $\mathbb{N}^+$ or ‹csucc(nat)›.›

theorem extension_pow_top:
  shows "(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){is a topology}"
proof-
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto 
  {
    fix M assume M:"M⊆(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
    let ?MP="{U∈M. U∈Pow(csucc(nat))}"
    let ?MN="{U∈M. U∉Pow(csucc(nat))}"
    have unM:"⋃M=(⋃?MP)∪(⋃?MN)" by auto
    have "csucc(nat)∉csucc(nat)" using mem_not_refl by auto
    with M have MN:"?MN={U∈M. U∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}}" by auto
    have unMP:"⋃?MP∈Pow(csucc(nat))" by auto
    then have "?MN=0⟶⋃M∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
      using unM by auto moreover
    {
      assume "?MN≠0"
      with MN have "{U∈M. U∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}}≠0" by auto
      then obtain U where U:"U∈M" "U∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by blast
      then obtain S where S:"U={csucc(nat)}∪S" "S∈(CoCountable csucc(nat))-{0}" by auto
      with U MN have "csucc(nat)∈U" "U∈?MN" by auto
      then have a1:"csucc(nat)∈⋃?MN" by auto
      let ?SC="{S∈(CoCountable csucc(nat)). {csucc(nat)}∪S∈M}"
      have unSC:"⋃?SC∈(CoCountable csucc(nat))" using CoCar_is_topology[OF InfCard_csucc[OF InfCard_nat]]
        unfolding IsATopology_def unfolding Cocountable_def by blast
      {
        fix s assume "s∈{csucc(nat)}∪⋃?SC"
        then have "s=csucc(nat)∨s∈⋃?SC" by auto
        then have "s∈⋃?MN∨(∃S∈?SC. s∈S)" using a1 by auto
        then have "s∈⋃?MN∨(∃S∈(CoCountable csucc(nat)). {csucc(nat)}∪S∈M ∧ s∈S)" by auto
        with MN have "s∈⋃?MN∨(∃S∈(CoCountable csucc(nat)). {csucc(nat)}∪S∈?MN ∧ s∈S)" by auto
        then have "s∈⋃?MN" by blast
      }
      then have "{csucc(nat)}∪⋃?SC⊆⋃?MN" by blast
      moreover
      {
        fix s assume "s∈⋃?MN"
        then obtain U where U:"s∈U" "U∈M" "U∉Pow(csucc(nat))" by auto
        with M have "U∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))}" by auto
        then obtain S where S:"U={csucc(nat)}∪S" "S∈(CoCountable csucc(nat))" by auto
        with U(1) have "s=csucc(nat)∨s∈S" by auto
        with S U(2) have "s=csucc(nat)∨s∈⋃?SC" by auto
        then have "s∈{csucc(nat)}∪⋃?SC" by auto
      }
      then have "⋃?MN⊆{csucc(nat)}∪⋃?SC" by blast
      ultimately have unMN:"⋃?MN={csucc(nat)}∪⋃?SC" by auto
      from unSC have b1:"csucc(nat)-⋃?SC≺csucc(nat)∨⋃?SC=0" unfolding Cocountable_def CoCardinal_def
        by auto
      {
        assume "0∈?SC"
        then have "{csucc(nat)}∈M" by auto
        then have "{csucc(nat)}∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" using mem_not_refl
          M by auto
        then obtain S where S:"S∈(CoCountable csucc(nat))-{0}" "{csucc(nat)}={csucc(nat)}∪S" by auto
        {
          fix x assume "x∈S"
          then have "x∈{csucc(nat)}∪S" by auto
          with S(2) have "x∈{csucc(nat)}" by auto
          then have "x=csucc(nat)" by auto
        }
        then have "S⊆{csucc(nat)}" by auto
        with S(1) have "S={csucc(nat)}" by auto
        with S(1) have "csucc(nat)-{csucc(nat)}≺csucc(nat)" unfolding Cocountable_def CoCardinal_def
          by auto moreover
        then have "csucc(nat)-{csucc(nat)}=csucc(nat)" using mem_not_refl[of "csucc(nat)"] by force
        ultimately have "False" by auto
      }
      then have "0∉?SC" by auto moreover
      from S U(1) have "S∈?SC" by auto
      ultimately have "S⊆⋃?SC" "S≠0" by auto
      then have noe:"⋃?SC≠0" by auto
      with b1 have "csucc(nat)-⋃?SC≺csucc(nat)" by auto
      moreover have "csucc(nat)-(⋃?SC ∪ ⋃?MP)⊆csucc(nat)-⋃?SC" by auto
      then have "csucc(nat)-(⋃?SC ∪ ⋃?MP)≲csucc(nat)-⋃?SC" using subset_imp_lepoll by auto
      ultimately have "csucc(nat)-(⋃?SC ∪ ⋃?MP)≺csucc(nat)" using lesspoll_trans1 by auto moreover
      have "⋃?SC⊆⋃(CoCountable csucc(nat))" using unSC by auto
      then have "⋃?SC⊆csucc(nat)" using union_cocardinal[OF noE] unfolding Cocountable_def by auto
      ultimately have "(⋃?SC ∪ ⋃?MP)∈(CoCountable csucc(nat))"
        using unMP unfolding Cocountable_def CoCardinal_def by auto
      then have "{csucc(nat)}∪(⋃?SC ∪ ⋃?MP)∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
        using noe by auto moreover
      from unM unMN have "⋃M=({csucc(nat)}∪⋃?SC) ∪ ⋃?MP" by auto
      then have "⋃M={csucc(nat)}∪(⋃?SC ∪ ⋃?MP)" by auto
      ultimately have "⋃M∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
    }
    ultimately have "⋃M∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  }
  then have "∀M∈Pow(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}). ⋃M∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  moreover
  {
    fix U V assume UV:"U∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" "V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
    {
      assume "csucc(nat)∉U∨csucc(nat)∉V"
      with UV have "U∈Pow(csucc(nat))∨V∈Pow(csucc(nat))" by auto
      then have "U∩V∈Pow(csucc(nat))" by auto
      then have "U∩V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
    }
    moreover
    {
      assume "csucc(nat)∈U∧csucc(nat)∈V"
      then obtain SU SV where S:"U={csucc(nat)}∪SU" "V={csucc(nat)}∪SV" "SU∈(CoCountable csucc(nat))-{0}"
        "SV∈(CoCountable csucc(nat))-{0}" using UV mem_not_refl by auto
      from S(1,2) have "U∩V={csucc(nat)}∪(SU∩SV)" by auto moreover
      from S(3,4) have "SU∩SV∈(CoCountable csucc(nat))" using CoCar_is_topology[OF InfCard_csucc[OF InfCard_nat]] unfolding IsATopology_def
        unfolding Cocountable_def by blast moreover
      from S(3,4) have "SU∩SV≠0" using cocountable_in_csucc_nat_HConn unfolding IsHConnected_def
        by auto ultimately
      have "U∩V∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
      then have "U∩V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
    }
    ultimately have "U∩V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  }
  then have "∀U∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}). ∀V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}). U∩V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  ultimately show ?thesis unfolding IsATopology_def by auto
qed

text‹This topology is defined over $\mathbb{N}^+\cup\{\mathbb{N}^+\}$ or ‹csucc(nat)∪{csucc(nat)}›.›

lemma extension_pow_union:
  shows "⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})=csucc(nat)∪{csucc(nat)}"
proof
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto 
  have "⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})=⋃(Pow(csucc(nat))) ∪ (⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
    by blast
  also have "…=csucc(nat) ∪ (⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  ultimately have A:"⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})=csucc(nat) ∪ (⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  have "⋃(CoCountable csucc(nat))∈(CoCountable csucc(nat))" using CoCar_is_topology[OF InfCard_csucc[OF InfCard_nat]]
    unfolding IsATopology_def Cocountable_def by auto
  then have "csucc(nat)∈(CoCountable csucc(nat))" using union_cocardinal[OF noE] unfolding Cocountable_def
    by auto
  with noE have "csucc(nat)∈(CoCountable csucc(nat))-{0}" by auto
  then have "{csucc(nat)}∪csucc(nat)∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
  then have "{csucc(nat)}∪csucc(nat)⊆⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by blast
  with A show "csucc(nat)∪{csucc(nat)}⊆⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
    by auto
  {
    fix x assume x:"x∈(⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" "x≠csucc(nat)"
    then obtain U where U:"U∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" "x∈U" by blast
    then obtain S where S:"U={csucc(nat)}∪S" "S∈(CoCountable csucc(nat))-{0}" by auto
    with U(2) x(2) have "x∈S" by auto
    with S(2) have "x∈⋃(CoCountable csucc(nat))" by auto
    then have "x∈csucc(nat)" using union_cocardinal[OF noE] unfolding Cocountable_def by auto
  }
  then have "(⋃{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})⊆csucc(nat) ∪{csucc(nat)}" by blast
  with A show "⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})⊆csucc(nat)∪{csucc(nat)}"
    by blast
qed

text‹This topology has a discrete open subspace.›

lemma extension_pow_subspace:
  shows "(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)=Pow(csucc(nat))"
  and "csucc(nat)∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
proof
  show "csucc(nat)∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
  {
    fix x assume "x∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)"
    then obtain R where "x=csucc(nat)∩R" "R∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" unfolding RestrictedTo_def
      by auto
    then have "x∈Pow(csucc(nat))" by auto
  }
  then show "(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)⊆Pow(csucc(nat))" by auto
  {
    fix x assume x:"x∈Pow(csucc(nat))"
    then have "x=csucc(nat)∩x" by auto
    with x have "x∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)"
      unfolding RestrictedTo_def by auto
  }
  then show "Pow(csucc(nat))⊆(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)" by auto
qed

text‹This topology is Hausdorff.›

theorem extension_pow_T2:
  shows "(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){is T⇩2}"
proof-
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto 
  {
    fix A B assume "A∈⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
      "B∈⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" "A≠B"
    then have AB:"A∈csucc(nat)∪{csucc(nat)}" "B∈csucc(nat)∪{csucc(nat)}" "A≠B" using extension_pow_union by auto
    {
      assume "A≠csucc(nat)" "B≠csucc(nat)"
      then have "A∈csucc(nat)" "B∈csucc(nat)" using AB by auto
      then have sub:"{A}∈Pow(csucc(nat))" "{B}∈Pow(csucc(nat))" by auto
      then have "{A}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)" 
        "{B}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)" using extension_pow_subspace(1)
        by auto 
      then obtain RA RB where "{A}=csucc(nat)∩RA" "{B}=csucc(nat)∩RB" "RA∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
        "RB∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" unfolding RestrictedTo_def by auto
      then have "{A}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" "{B}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
        using extension_pow_subspace(2) extension_pow_top unfolding IsATopology_def by auto
      moreover
      from AB(3) have "{A}∩{B}=0" by auto ultimately
      have "∃U∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}). ∃V∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}). A∈U∧B∈V∧U∩V=0" by auto
    }
    moreover
    {
      assume "A=csucc(nat)∨B=csucc(nat)"
      with AB(3) have disj:"(A=csucc(nat)∧B≠csucc(nat))∨(B=csucc(nat)∧A≠csucc(nat))" by auto
      {
        assume ass:"A=csucc(nat)∧B≠csucc(nat)" 
        then have p:"B∈csucc(nat)" using AB(2) by auto
        have "{B}≈1" using singleton_eqpoll_1 by auto
        then have "{B}≺nat" using eq_lesspoll_trans n_lesspoll_nat by auto
        then have "{B}≲nat" using lesspoll_imp_lepoll by auto
        then have "{B}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
        with p have "{B}{is closed in}(CoCountable csucc(nat))" unfolding Cocountable_def
          using closed_sets_cocardinal[OF noE] by auto
        then have "csucc(nat)-{B}∈(CoCountable csucc(nat))" unfolding IsClosed_def
          Cocountable_def using union_cocardinal[OF noE] by auto moreover
        {
          assume "csucc(nat)-{B}=0"
          with p have "csucc(nat)={B}" by auto
          then have "csucc(nat)≈1" using singleton_eqpoll_1 by auto
          then have "csucc(nat)≲nat" using eq_lesspoll_trans n_lesspoll_nat lesspoll_imp_lepoll by auto
          then have "csucc(nat)≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
          then have "False" by auto
        }
        ultimately
        have "{csucc(nat)}∪(csucc(nat)-{B})∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
        then have U1:"{csucc(nat)}∪(csucc(nat)-{B})∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
        have "{B}∈Pow(csucc(nat))" using p by auto
        then have "{B}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)"
          using extension_pow_subspace(1) by auto
        then obtain R where "R∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" "{B}=csucc(nat)∩R"
          unfolding RestrictedTo_def by auto
        then have U2:"{B}∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" using extension_pow_subspace(2)
          extension_pow_top unfolding IsATopology_def by auto
        have "({csucc(nat)}∪(csucc(nat)-{B}))∩{B}=0" using p mem_not_refl[of "csucc(nat)"] by auto
        with U1 U2 have "∃U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}. ∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧B∈V∧U∩V=0" using ass(1) by auto
      }
      moreover
      {
        assume "¬(A=csucc(nat)∧B≠csucc(nat))" 
        then have ass:"B = csucc(nat) ∧ A ≠ csucc(nat)" using disj by auto
        then have p:"A∈csucc(nat)" using AB(1) by auto
        have "{A}≈1" using singleton_eqpoll_1 by auto
        then have "{A}≺nat" using eq_lesspoll_trans n_lesspoll_nat by auto
        then have "{A}≲nat" using lesspoll_imp_lepoll by auto
        then have "{A}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
        with p have "{A}{is closed in}(CoCountable csucc(nat))" unfolding Cocountable_def
          using closed_sets_cocardinal[OF noE] by auto
        then have "csucc(nat)-{A}∈(CoCountable csucc(nat))" unfolding IsClosed_def
          Cocountable_def using union_cocardinal[OF noE] by auto moreover
        {
          assume "csucc(nat)-{A}=0"
          with p have "csucc(nat)={A}" by auto
          then have "csucc(nat)≈1" using singleton_eqpoll_1 by auto
          then have "csucc(nat)≲nat" using eq_lesspoll_trans n_lesspoll_nat lesspoll_imp_lepoll by auto
          then have "csucc(nat)≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
          then have "False" by auto
        }
        ultimately
        have "{csucc(nat)}∪(csucc(nat)-{A})∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
        then have U1:"{csucc(nat)}∪(csucc(nat)-{A})∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
        have "{A}∈Pow(csucc(nat))" using p by auto
        then have "{A}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat)"
          using extension_pow_subspace(1) by auto
        then obtain R where "R∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" "{A}=csucc(nat)∩R"
          unfolding RestrictedTo_def by auto
        then have U2:"{A}∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" using extension_pow_subspace(2)
          extension_pow_top unfolding IsATopology_def by auto
        have int:"{A}∩({csucc(nat)}∪(csucc(nat)-{A}))=0" using p mem_not_refl[of "csucc(nat)"] by auto
        have "A∈{A}" "csucc(nat)∈({csucc(nat)}∪(csucc(nat)-{A}))" by auto
        with int U1 have "∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈{A}∧csucc(nat)∈V∧{A}∩V=0" by auto
        with U2 have "∃U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}. ∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧csucc(nat)∈V∧U∩V=0" using exI[where P="λU. U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}∧(∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧csucc(nat)∈V∧U∩V=0)" and x="{A}"] unfolding Bex_def by auto
        then have "∃U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}. ∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧B∈V∧U∩V=0" using ass by auto
      } 
      ultimately have "∃U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}. ∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧B∈V∧U∩V=0" by auto
    }
    ultimately have "∃U∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}. ∃V∈Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}.
          A∈U∧B∈V∧U∩V=0" by auto
  }
  then show ?thesis unfolding isT2_def by auto
qed

text‹The topology we built is not discrete; i.e., not every set is open.›

theorem extension_pow_notDiscrete:
  shows "{csucc(nat)}∉(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
proof
  assume "{csucc(nat)}∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
  then have "{csucc(nat)}∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" using mem_not_refl by auto
  then obtain S where S:"S∈(CoCountable csucc(nat))-{0}" "{csucc(nat)}={csucc(nat)}∪S" by auto
  {
    fix x assume "x∈S"
    then have "x∈{csucc(nat)}∪S" by auto
    with S(2) have "x∈{csucc(nat)}" by auto
    then have "x=csucc(nat)" by auto
  }
  then have "S⊆{csucc(nat)}" by auto
  with S(1) have "S={csucc(nat)}" by auto
  with S(1) have "csucc(nat)-{csucc(nat)}≺csucc(nat)" unfolding Cocountable_def CoCardinal_def
    by auto moreover
  then have "csucc(nat)-{csucc(nat)}=csucc(nat)" using mem_not_refl[of "csucc(nat)"] by force
  ultimately show "False" by auto
qed

text‹The topology we built is anti-compact.›

theorem extension_pow_antiCompact:
  shows "(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){is anti-compact}"
proof-
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto 
  {
    fix K assume K:"K⊆⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" 
      "(⋃((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}K)){is compact in}((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}K)"
    from K(1) have sub:"K⊆csucc(nat) ∪{csucc(nat)}" using extension_pow_union by auto
    have "(⋃((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}K))=(csucc(nat) ∪{csucc(nat)})∩K"
      using extension_pow_union unfolding RestrictedTo_def by auto moreover
    from sub have "(csucc(nat) ∪{csucc(nat)})∩K=K" by auto
    ultimately have "(⋃((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}K))=K" by auto
    with K(2) have "K{is compact in}((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}K)" by auto
    then have comp:"K{is compact in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" using 
      compact_subspace_imp_compact by auto
    {
      assume ss:"K⊆csucc(nat)"
      then have "K{is compact in}((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat))"
        using compact_imp_compact_subspace comp Compact_is_card_nat by auto
      then have "K{is compact in}Pow(csucc(nat))" using extension_pow_subspace(1) by auto
      then have "K{is compact in}(Pow(csucc(nat)){restricted to}K)" using compact_imp_compact_subspace
        Compact_is_card_nat by auto moreover
      have "⋃(Pow(csucc(nat)){restricted to}K)=K" using ss unfolding RestrictedTo_def by auto
      ultimately have "(⋃(Pow(csucc(nat)){restricted to}K)){is compact in}(Pow(csucc(nat)){restricted to}K)" by auto
      then have "K{is in the spectrum of}(λT. (⋃T){is compact in}T)" using pow_anti_compact 
        unfolding IsAntiComp_def antiProperty_def using ss by auto
    }
    moreover
    {
      assume "¬(K⊆csucc(nat))"
      with sub have "csucc(nat)∈K" by auto
      with sub have ss:"K-{csucc(nat)}⊆csucc(nat)" by auto
      {
        assume prec:"K-{csucc(nat)}≺csucc(nat)"
        then have "(K-{csucc(nat)}){is closed in}(CoCountable csucc(nat))"
          using closed_sets_cocardinal[OF noE] ss unfolding Cocountable_def by auto
        then have "csucc(nat)-(K-{csucc(nat)})∈(CoCountable csucc(nat))" unfolding IsClosed_def
          Cocountable_def using union_cocardinal[OF noE] by auto moreover
        {
          assume "csucc(nat)-(K-{csucc(nat)})=0"
          with ss have "csucc(nat)=(K-{csucc(nat)})" by auto
          with prec have "False" by auto
        }
        ultimately have "{csucc(nat)} ∪(csucc(nat)-(K-{csucc(nat)}))∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}"
          by auto
        moreover have "{csucc(nat)} ∪(csucc(nat)-(K-{csucc(nat)}))=({csucc(nat)} ∪ csucc(nat))-(K-{csucc(nat)})" by blast
        ultimately have "({csucc(nat)} ∪ csucc(nat))-(K-{csucc(nat)})∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
        then have "({csucc(nat)} ∪ csucc(nat))-(K-{csucc(nat)})∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          by auto moreover
        have "csucc(nat) ∪ {csucc(nat)}={csucc(nat)} ∪ csucc(nat)" by auto
        ultimately have "(csucc(nat) ∪ {csucc(nat)})-(K-{csucc(nat)})∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          by auto
        then have "(⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}))-(K-{csucc(nat)})∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          using extension_pow_union by auto
        then have "(K-{csucc(nat)}){is closed in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          unfolding IsClosed_def using ss by auto
        with comp have "(K∩(K-{csucc(nat)})){is compact in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" using compact_closed
          Compact_is_card_nat by auto
        moreover have "K∩(K-{csucc(nat)})=(K-{csucc(nat)})" by auto
        ultimately have "(K-{csucc(nat)}){is compact in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
        with ss have "(K-{csucc(nat)}){is compact in}((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat))"
          using compact_imp_compact_subspace comp Compact_is_card_nat by auto
        then have "(K-{csucc(nat)}){is compact in}(Pow(csucc(nat)))" using extension_pow_subspace(1) by auto
        then have "(K-{csucc(nat)}){is compact in}(Pow(csucc(nat)){restricted to}(K-{csucc(nat)}))" using compact_imp_compact_subspace
          Compact_is_card_nat by auto moreover
        have "⋃(Pow(csucc(nat)){restricted to}(K-{csucc(nat)}))=(K-{csucc(nat)})" using ss unfolding RestrictedTo_def by auto
        ultimately have "(⋃(Pow(csucc(nat)){restricted to}(K-{csucc(nat)}))){is compact in}(Pow(csucc(nat)){restricted to}(K-{csucc(nat)}))" by auto
        then have "(K-{csucc(nat)}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using pow_anti_compact 
          unfolding IsAntiComp_def antiProperty_def using ss by auto
        then have "Finite(K-{csucc(nat)})" using compact_spectrum by auto moreover
        have "Finite({csucc(nat)})" by auto ultimately
        have "Finite(K)" using Diff_Finite[of "{csucc(nat)}" "K"] by auto
        then have "K{is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
      }
      moreover
      {
        assume "¬(K-{csucc(nat)}≺csucc(nat))"
        with ss have "K-{csucc(nat)}≈csucc(nat)" using lepoll_iff_leqpoll subset_imp_lepoll[of "K-{csucc(nat)}"
          "csucc(nat)"] by auto
        then have "csucc(nat)≈K-{csucc(nat)}" using eqpoll_sym by auto
        then have "nat≺K-{csucc(nat)}" using lesspoll_eq_trans lt_csucc[OF Ord_nat]
          lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]] by auto
        then have "nat≲K-{csucc(nat)}" using lepoll_iff_leqpoll by auto
        then obtain f where "f∈inj(nat,K-{csucc(nat)})" unfolding lepoll_def by auto moreover
        then have fun:"f:nat→K-{csucc(nat)}" unfolding inj_def by auto
        then have "f∈surj(nat,range(f))" using fun_is_surj by auto
        ultimately have "f∈bij(nat,range(f))" unfolding bij_def inj_def surj_def by auto
        then have "nat≈range(f)" unfolding eqpoll_def by auto
        then have e:"range(f)≈nat" using eqpoll_sym by auto
        then have as2:"range(f)≺csucc(nat)" using lt_Card_imp_lesspoll[OF Card_csucc[OF Ord_nat]]
          lt_csucc[OF Ord_nat] eq_lesspoll_trans by auto
        then have "range(f){is closed in}(CoCountable csucc(nat))" using closed_sets_cocardinal[of "csucc(nat)"
            "range(f)""csucc(nat)"] unfolding Cocountable_def using func1_1_L5B[OF fun] ss noE by auto
        then have "csucc(nat)-(range(f))∈(CoCountable csucc(nat))" unfolding IsClosed_def
          Cocountable_def using union_cocardinal[OF noE] by auto moreover
        {
          assume "csucc(nat)-(range(f))=0"
          with ss func1_1_L5B[OF fun] have "csucc(nat)=(range(f))" by blast
          with as2 have "False" by auto
        }
        ultimately have "{csucc(nat)} ∪(csucc(nat)-(range(f)))∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}"
          by auto
        moreover have "{csucc(nat)} ∪(csucc(nat)-(range(f)))=({csucc(nat)} ∪ csucc(nat))-(range(f))" using func1_1_L5B[OF fun] by blast
        ultimately have "({csucc(nat)} ∪ csucc(nat))-(range(f))∈{{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" by auto
        then have "({csucc(nat)} ∪ csucc(nat))-(range(f))∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          by auto moreover
        have "csucc(nat) ∪ {csucc(nat)}={csucc(nat)} ∪ csucc(nat)" by auto
        ultimately have "(csucc(nat) ∪ {csucc(nat)})-(range(f))∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          by auto
        then have "(⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}))-(range(f))∈(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          using extension_pow_union by auto moreover
        have "range(f)⊆⋃(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" using ss func1_1_L5B[OF fun] by auto
        ultimately have "(range(f)){is closed in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
          unfolding IsClosed_def by blast
        with comp have "(K∩(range(f))){is compact in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" using compact_closed
          Compact_is_card_nat by auto
        moreover have "K∩(range(f))=(range(f))" using func1_1_L5B[OF fun] by auto
        ultimately have "(range(f)){is compact in}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})" by auto
        with ss func1_1_L5B[OF fun] have "(range(f)){is compact in}((Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}){restricted to}csucc(nat))"
          using compact_imp_compact_subspace[of "range(f)" "nat" "Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}}" "csucc(nat)"] comp Compact_is_card_nat by auto
        then have "(range(f)){is compact in}(Pow(csucc(nat)))" using extension_pow_subspace(1) by auto
        then have "(range(f)){is compact in}(Pow(csucc(nat)){restricted to}(range(f)))" using compact_imp_compact_subspace
          Compact_is_card_nat by auto moreover
        have "⋃(Pow(csucc(nat)){restricted to}(range(f)))=(range(f))" using ss func1_1_L5B[OF fun] unfolding RestrictedTo_def by auto
        ultimately have "(⋃(Pow(csucc(nat)){restricted to}(range(f)))){is compact in}(Pow(csucc(nat)){restricted to}(range(f)))" by auto
        then have "(range(f)){is in the spectrum of}(λT. (⋃T){is compact in}T)" using pow_anti_compact[of "csucc(nat)"]
          unfolding IsAntiComp_def antiProperty_def using ss func1_1_L5B[OF fun] by auto
        then have "Finite(range(f))" using compact_spectrum by auto moreover
        then have "Finite(nat)" using e eqpoll_imp_Finite_iff by auto ultimately
        have "False" using nat_not_Finite by auto
      }
      ultimately have "K {is in the spectrum of}( λT. (⋃T) {is compact in} T)" by auto
    }
    ultimately have "K {is in the spectrum of}( λT. (⋃T) {is compact in} T)" by auto
  }
  then show ?thesis unfolding IsAntiComp_def antiProperty_def by auto
qed

text‹If a topological space is KC, then its one-point compactification
is US.›

theorem (in topology0) KC_imp_OP_comp_is_US:
  assumes "T{is KC}"
  shows "({one-point compactification of}T){is US}"
proof-
  {
    fix N x y assume A:"N:nat→⋃({one-point compactification of}T)" "⟨N,Le⟩→⇩N x{in}({one-point compactification of}T)" "⟨N,Le⟩→⇩N y{in}({one-point compactification of}T)" "x≠y"
    have dir:"Le directs nat" using Le_directs_nat(2).
    from A(1) have dom:"domain(N)=nat" using func1_1_L1 by auto
    with dir A(1) have NET:"⟨N,Le⟩{is a net on}⋃({one-point compactification of}T)" unfolding IsNet_def by auto
    have xy:"x∈⋃({one-point compactification of}T)" "y∈⋃({one-point compactification of}T)"
      using A(2,3) topology0.NetConverges_def[OF _ NET] unfolding topology0_def using op_comp_is_top dom by auto 
    then have pp:"x∈⋃T ∪{⋃T}" "y∈⋃T ∪{⋃T}" using op_compact_total by auto
    from A(2) have comp:"∀U∈Pow(⋃{one-point compactification of}T).
        x ∈ Interior(U, {one-point compactification of}T) ⟶
        (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U)" using topology0.NetConverges_def[OF _ NET, of "x"]
        unfolding topology0_def using op_comp_is_top dom op_compact_total by auto
    from A(3) have op2:"∀U∈Pow(⋃{one-point compactification of}T).
        y ∈ Interior(U, {one-point compactification of}T) ⟶
        (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U)" using topology0.NetConverges_def[OF _ NET, of "y"]
        unfolding topology0_def using op_comp_is_top dom op_compact_total by auto
    {
      assume p:"x∈⋃T" "y∈⋃T"
      {
        assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T"
        have "⋃T∈({one-point compactification of}T)" using open_subspace by auto
        then have "⋃T=Interior(⋃T,{one-point compactification of}T)" using topology0.Top_2_L3
          unfolding topology0_def using op_comp_is_top by auto
        then have "x∈Interior(⋃T,{one-point compactification of}T)" using p(1) by auto moreover
        have "⋃T∈Pow(⋃({one-point compactification of}T))" using open_subspace(1) by auto
        ultimately have "∃t∈domain(fst(⟨N, Le⟩)). ∀m∈domain(fst(⟨N, Le⟩)). ⟨t, m⟩ ∈ snd(⟨N, Le⟩) ⟶ fst(⟨N, Le⟩) ` m ∈ ⋃T" using A(2)
          using topology0.NetConverges_def[OF _ NET] op_comp_is_top unfolding topology0_def by blast
        then have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" using dom by auto
        then obtain t where t:"t∈nat" "∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" by auto
        from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T" by auto
        from t(1) n(1) dir obtain z where z:"z∈nat" "⟨n,z⟩∈Le" "⟨t,z⟩∈Le" unfolding IsDirectedSet_def
          by auto
        from t(2) z(1,3) have "N`z∈⋃T" by auto moreover
        from n(2) z(1,2) have "N`z=⋃T" by auto ultimately
        have "False" using mem_not_refl by auto
      }
      then have reg:"∀n∈nat. ∃m∈nat. N`m≠⋃T ∧ ⟨n,m⟩∈Le" by auto
      let ?NN="{⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩. n∈nat}"
      {
        fix x z assume A1:"⟨x, z⟩ ∈ ?NN"
        {
          fix y' assume A2:"⟨x,y'⟩∈?NN"
          with A1 have "z=y'" by auto
        }
        then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto
      }
      then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto
      moreover
      {
      fix n assume as:"n∈nat"
        with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
        then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
          nat_into_Ord[of "m"] by auto
        then have "(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈nat" by auto
        then have "N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈⋃({one-point compactification of}T)" using apply_type[OF A(1)] op_compact_total by auto
        with as have "⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃({one-point compactification of}T)" by auto
      }
      then have "?NN∈Pow(nat×⋃({one-point compactification of}T))" by auto
      ultimately have NFun:"?NN:nat→⋃({one-point compactification of}T)" unfolding Pi_def function_def domain_def by auto
      {
        fix n assume as:"n∈nat"
        with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
        then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
          nat_into_Ord[of "m"] by auto
        then have "?NN`n≠⋃T" using apply_equality[OF _ NFun] by auto
      }
      then have noy:"∀n∈nat. ?NN`n≠⋃T" by auto
      then have "∀n∈nat. ?NN`n∈⋃T" using apply_type[OF NFun] op_compact_total by auto
      then have R:"?NN:nat→⋃T" using func1_1_L1A[OF NFun] by auto
      have dom2:"domain(?NN)=nat" by auto
      then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using R dir by auto
      {
        fix U assume U:"U⊆⋃T" "x∈int(U)"
        have intT:"int(U)∈T" using Top_2_L2 by auto
        then have "int(U)∈({one-point compactification of}T)" unfolding OPCompactification_def
          by auto
        then have "Interior(int(U),{one-point compactification of}T)=int(U)" using topology0.Top_2_L3
          unfolding topology0_def using op_comp_is_top by auto
        with U(2) have "x∈Interior(int(U),{one-point compactification of}T)" by auto
        with intT have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈int(U))" using comp op_compact_total by auto
        then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using Top_2_L1 by auto
        {
          fix s assume AA:"⟨r,s⟩∈Le"
          with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
          then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
            nat_into_Ord by auto
          with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
          with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈U" by blast
          then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
        }
        then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
        with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
      }
      then have "∀U∈Pow(⋃T). x ∈ int(U)
        ⟶ (∃r∈nat. ∀s∈nat. ⟨r, s⟩ ∈ Le ⟶ ?NN ` s ∈ U)" by auto
      then have conx:"⟨?NN,Le⟩→⇩N x{in}T" using NetConverges_def[OF net2] p(1) op_comp_is_top 
        unfolding topology0_def using xy(1) dom2 by auto
      {
        fix U assume U:"U⊆⋃T" "y∈int(U)"
        have intT:"int(U)∈T" using Top_2_L2 by auto
        then have "int(U)∈({one-point compactification of}T)" unfolding OPCompactification_def
          by auto
        then have "Interior(int(U),{one-point compactification of}T)=int(U)" using topology0.Top_2_L3
          unfolding topology0_def using op_comp_is_top by auto
        with U(2) have "y∈Interior(int(U),{one-point compactification of}T)" by auto
        with intT have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈int(U))" using op2 op_compact_total by auto
        then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using Top_2_L1 by auto
        {
          fix s assume AA:"⟨r,s⟩∈Le"
          with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
          then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
            nat_into_Ord by auto
          with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
          with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈U" by blast
          then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
        }
        then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
        with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
      }
      then have "∀U∈Pow(⋃T). y ∈ int(U)
        ⟶ (∃r∈nat. ∀s∈nat. ⟨r, s⟩ ∈ Le ⟶ ?NN ` s ∈ U)" by auto
      then have cony:"⟨?NN,Le⟩→⇩N y{in}T" using NetConverges_def[OF net2] p(2) op_comp_is_top 
        unfolding topology0_def using xy(2) dom2 by auto
      with conx assms have "x=y" using KC_imp_US unfolding IsUS_def using R by auto
      with A(4) have "False" by auto
    }
    moreover
    {
      assume AAA:"x∉⋃T∨y∉⋃T"
      with pp have "x=⋃T∨y=⋃T" by auto
      {
        assume x:"x=⋃T"
        with A(4) have y:"y∈⋃T" using pp(2) by auto
        {
          assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T"
          have "⋃T∈({one-point compactification of}T)" using open_subspace by auto
          then have "⋃T=Interior(⋃T,{one-point compactification of}T)" using topology0.Top_2_L3
            unfolding topology0_def using op_comp_is_top by auto
          then have "y∈Interior(⋃T,{one-point compactification of}T)" using y by auto moreover
          have "⋃T∈Pow(⋃({one-point compactification of}T))" using open_subspace(1) by auto
          ultimately have "∃t∈domain(fst(⟨N, Le⟩)). ∀m∈domain(fst(⟨N, Le⟩)). ⟨t, m⟩ ∈ snd(⟨N, Le⟩) ⟶ fst(⟨N, Le⟩) ` m ∈ ⋃T" using A(3)
            using topology0.NetConverges_def[OF _ NET] op_comp_is_top unfolding topology0_def by blast
          then have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" using dom by auto
          then obtain t where t:"t∈nat" "∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" by auto
          from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T" by auto
          from t(1) n(1) dir obtain z where z:"z∈nat" "⟨n,z⟩∈Le" "⟨t,z⟩∈Le" unfolding IsDirectedSet_def
            by auto
          from t(2) z(1,3) have "N`z∈⋃T" by auto moreover
          from n(2) z(1,2) have "N`z=⋃T" by auto ultimately
          have "False" using mem_not_refl by auto
        }
        then have reg:"∀n∈nat. ∃m∈nat. N`m≠⋃T ∧ ⟨n,m⟩∈Le" by auto
        let ?NN="{⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩. n∈nat}"
        {
          fix x z assume A1:"⟨x, z⟩ ∈ ?NN"
          {
            fix y' assume A2:"⟨x,y'⟩∈?NN"
            with A1 have "z=y'" by auto
          }
          then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto
        }
        then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto
        moreover
        {
          fix n assume as:"n∈nat"
          with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
          then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
            nat_into_Ord[of "m"] by auto
          then have "(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈nat" by auto
          then have "N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈⋃({one-point compactification of}T)" using apply_type[OF A(1)] op_compact_total by auto
          with as have "⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃({one-point compactification of}T)" by auto
        }
        then have "?NN∈Pow(nat×⋃({one-point compactification of}T))" by auto
        ultimately have NFun:"?NN:nat→⋃({one-point compactification of}T)" unfolding Pi_def function_def domain_def by auto
        {
          fix n assume as:"n∈nat"
          with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
          then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
            nat_into_Ord[of "m"] by auto
          then have "?NN`n≠⋃T" using apply_equality[OF _ NFun] by auto
        }
        then have noy:"∀n∈nat. ?NN`n≠⋃T" by auto
        then have "∀n∈nat. ?NN`n∈⋃T" using apply_type[OF NFun] op_compact_total by auto
        then have R:"?NN:nat→⋃T" using func1_1_L1A[OF NFun] by auto
        have dom2:"domain(?NN)=nat" by auto
        then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using R dir by auto
        {
          fix U assume U:"U⊆⋃T" "y∈int(U)"
          have intT:"int(U)∈T" using Top_2_L2 by auto
          then have "int(U)∈({one-point compactification of}T)" unfolding OPCompactification_def
            by auto
          then have "Interior(int(U),{one-point compactification of}T)=int(U)" using topology0.Top_2_L3
            unfolding topology0_def using op_comp_is_top by auto
          with U(2) have "y∈Interior(int(U),{one-point compactification of}T)" by auto
          with intT have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈int(U))" using op2 op_compact_total by auto
          then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using Top_2_L1 by auto
          {
            fix s assume AA:"⟨r,s⟩∈Le"
            with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
            then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
              nat_into_Ord by auto
            with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
            with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈U" by blast
            then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
          }
          then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
          with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
        }
        then have "∀U∈Pow(⋃T). y ∈ int(U)
          ⟶ (∃r∈nat. ∀s∈nat. ⟨r, s⟩ ∈ Le ⟶ ?NN ` s ∈ U)" by auto
        then have cony:"⟨?NN,Le⟩→⇩N y{in}T" using NetConverges_def[OF net2] y op_comp_is_top 
          unfolding topology0_def using xy(2) dom2 by auto
        let ?A="{y}∪?NN``nat"
        {
          fix M assume Acov:"?A⊆⋃M" "M⊆T"
          then have "y∈⋃M" by auto
          then obtain V where V:"y∈V" "V∈M" by auto
          with Acov(2) have VT:"V∈T" by auto
          then have "V=int(V)" using Top_2_L3 by auto
          with V(1) have "y∈int(V)" by auto
          with cony obtain r where rr:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈V"
            unfolding NetConverges_def[OF net2, of "y"] using dom2 VT y by auto
          have NresFun:"restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}):{n∈nat. ⟨n,r⟩∈Le}→⋃T" using restrict_fun
            [OF R, of "{n∈nat. ⟨n,r⟩∈Le}"] by auto
          then have "restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})∈surj({n∈nat. ⟨n,r⟩∈Le},range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})))"
            using fun_is_surj by auto moreover
          have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
          then have "{n∈nat. ⟨n,r⟩∈Le}≲nat" using subset_imp_lepoll by auto
          ultimately have "range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}))≲{n∈nat. ⟨n,r⟩∈Le}" using surj_fun_inv_2 by auto
          moreover
          have "{n∈nat. ⟨n,0⟩∈Le}={0}" by auto
          then have "Finite({n∈nat. ⟨n,0⟩∈Le})" by auto moreover
          {
            fix j assume as:"j∈nat" "Finite({n∈nat. ⟨n,j⟩∈Le})"
            {
              fix t assume "t∈{n∈nat. ⟨n,succ(j)⟩∈Le}"
              then have "t∈nat" "⟨t,succ(j)⟩∈Le" by auto
              then have "t≤succ(j)" by auto
              then have "t⊆succ(j)" using le_imp_subset by auto
              then have "t⊆j ∪{j}" using succ_explained by auto
              then have "j∈t∨t⊆j" by auto
              then have "j∈t∨t≤j" using subset_imp_le ‹t∈nat› ‹j∈nat› nat_into_Ord by auto
              then have "j ∪{j}⊆t∨t≤j" using ‹t∈nat› ‹j∈nat› nat_into_Ord unfolding Ord_def
                Transset_def by auto
              then have "succ(j)⊆t∨t≤j" using succ_explained by auto
              with ‹t⊆succ(j)› have "t=succ(j)∨t≤j" by auto
              with ‹t∈nat› ‹j∈nat› have "t∈{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
            }
            then have "{n∈nat. ⟨n,succ(j)⟩∈Le} ⊆{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
            moreover have "Finite({n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)})" using as(2) Finite_cons
              by auto
            ultimately have "Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" using subset_Finite by auto
          }
          then have "∀j∈nat. Finite({n∈nat. ⟨n,j⟩∈Le}) ⟶ Finite({n∈nat. ⟨n,succ(j)⟩∈Le})"
            by auto
          ultimately have "Finite(range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le})))"
            using lepoll_Finite[of "range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))"
              "{n ∈ nat . ⟨n, r⟩ ∈ Le}"] ind_on_nat[OF ‹r∈nat›, where P="λt. Finite({n∈nat. ⟨n,t⟩∈Le})"] by auto
          then have "Finite((restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using range_image_domain[OF NresFun]
            by auto
          then have "Finite(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using restrict_image by auto
          then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
          moreover have "⋃(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})=⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
            unfolding RestrictedTo_def by auto moreover
          have "⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}=?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
            using func1_1_L6(2)[OF R] by blast
          moreover have "(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is a topology}"
            using Top_1_L4 unfolding topology0_def by auto
          ultimately have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})"
            unfolding Spec_def by force
          then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T)" using compact_subspace_imp_compact by auto
          moreover from Acov(1) have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃M" by auto
          moreover note Acov(2) ultimately
          obtain 𝔑 where 𝔑:"𝔑∈FinPow(M)" "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃𝔑"
            unfolding IsCompact_def by blast
          from 𝔑(1) have "𝔑 ∪{V}∈FinPow(M)" using V(2) unfolding FinPow_def by auto moreover
          {
            fix s assume s:"s∈?A" "s∉V"
            with V(1) have "s∈?NN``nat" by auto
            then have "s∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
            then obtain n where n:"n∈nat" "s=?NN`n" by auto
            {
              assume "⟨r,n⟩∈Le"
              with rr have "?NN`n∈V" by auto
              with n(2) s(2) have "False" by auto
            }
            then have "⟨r,n⟩∉Le" by auto
            with rr(1) n(1) have "¬(r≤n)" by auto
            then have "n≤r" using Ord_linear_le[where thesis="⟨n,r⟩∈Le"] nat_into_Ord[OF rr(1)]
              nat_into_Ord[OF n(1)] by auto
            with rr(1) n(1) have "⟨n,r⟩∈Le" by auto
            with n(2) have "s∈{?NN`t. t∈{n∈nat. ⟨n,r⟩∈Le}}" by auto moreover
            have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
            ultimately have "s∈?NN``{n∈nat. ⟨n,r⟩∈Le}" using func_imagedef[OF NFun]
              by auto
            with 𝔑(2) have "s∈⋃𝔑" by auto
          }
          then have "?A⊆⋃𝔑 ∪ V" by auto
          then have "?A⊆⋃(𝔑 ∪ {V})" by auto ultimately
          have "∃𝔑∈FinPow(M). ?A⊆⋃𝔑" by auto
        }
        then have "∀M∈Pow(T). ?A⊆⋃M ⟶ (∃𝔑∈FinPow(M). ?A⊆⋃𝔑)" by auto moreover
        have ss:"?A⊆⋃(T)" using func1_1_L6(2)[OF R] y by blast ultimately
        have "?A{is compact in}(T)" unfolding IsCompact_def by auto moreover
        with assms have "?A{is closed in}(T)" unfolding IsKC_def IsCompact_def by auto ultimately
        have "?A∈{B∈Pow(⋃T). B{is compact in}(T)∧B{is closed in}(T)}" using ss by auto
        then have "{⋃T}∪(⋃T-?A)∈({one-point compactification of}T)" unfolding OPCompactification_def
          by auto
        then have "{⋃T}∪(⋃T-?A)=Interior({⋃T}∪(⋃T-?A),{one-point compactification of}T)" using topology0.Top_2_L3 op_comp_is_top
          unfolding topology0_def by auto moreover
        {
          assume "x∈?A"
          with A(4) have "x∈?NN``nat" by auto
          then have "x∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
          then obtain n where "n∈nat""?NN`n=x" by auto
          with noy x have "False" by auto
        }
        with y have "x∈{⋃T}∪(⋃T-?A)" using x by force ultimately
        have "x∈Interior({⋃T}∪(⋃T-?A),{one-point compactification of}T)" "{⋃T}∪(⋃T-?A)∈Pow(⋃({one-point compactification of}T))"
          using op_compact_total by auto moreover
        have "(∀U∈Pow(⋃({one-point compactification of}T)).  x ∈ Interior(U,{one-point compactification of}T) ⟶ (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U))"
          using A(2) dom topology0.NetConverges_def[OF _ NET] op_comp_is_top unfolding topology0_def by auto
        ultimately have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ {⋃T}∪(⋃T-?A)" by blast
        then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈{⋃T}∪(⋃T-?A)" by auto
        {
          fix s assume AA:"⟨r,s⟩∈Le"
          with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
          then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
            nat_into_Ord by auto
          with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
          with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈{⋃T}∪(⋃T-?A)" by auto
          then have "?NN`s∈{⋃T}∪(⋃T-?A)" using apply_equality[OF _ NFun] AA by auto
          with noy have "?NN`s∈(⋃T-?A)" using AA by auto
          moreover have "?NN`s∈{?NN`t. t∈nat}" using AA by auto
          then have "?NN`s∈?NN``nat" using func_imagedef[OF NFun] by auto
          then have "?NN`s∈?A" by auto
          ultimately have "False" by auto
        }
        moreover have "r⊆succ(r)" using succ_explained by auto
        then have "r≤succ(r)" using subset_imp_le nat_into_Ord ‹r∈nat› nat_succI
          by auto
        then have "⟨r,succ(r)⟩∈Le" using ‹r∈nat› nat_succI by auto
        ultimately have "False" by auto
      }
      then have "x≠⋃T" by auto
      with xy(1) AAA have "y∉⋃T" "x∈⋃T" using op_compact_total by auto
      with xy(2) have y:"y=⋃T" and x:"x∈⋃T" using op_compact_total by auto
      {
        assume B:"∃n∈nat. ∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T"
        have "⋃T∈({one-point compactification of}T)" using open_subspace by auto
        then have "⋃T=Interior(⋃T,{one-point compactification of}T)" using topology0.Top_2_L3
          unfolding topology0_def using op_comp_is_top by auto
        then have "x∈Interior(⋃T,{one-point compactification of}T)" using x by auto moreover
        have "⋃T∈Pow(⋃({one-point compactification of}T))" using open_subspace(1) by auto
        ultimately have "∃t∈domain(fst(⟨N, Le⟩)). ∀m∈domain(fst(⟨N, Le⟩)). ⟨t, m⟩ ∈ snd(⟨N, Le⟩) ⟶ fst(⟨N, Le⟩) ` m ∈ ⋃T" using A(2)
          using topology0.NetConverges_def[OF _ NET] op_comp_is_top unfolding topology0_def by blast
        then have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" using dom by auto
        then obtain t where t:"t∈nat" "∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ ⋃T" by auto
        from B obtain n where n:"n∈nat" "∀m∈nat. ⟨n,m⟩∈Le ⟶ N`m=⋃T" by auto
        from t(1) n(1) dir obtain z where z:"z∈nat" "⟨n,z⟩∈Le" "⟨t,z⟩∈Le" unfolding IsDirectedSet_def
          by auto
        from t(2) z(1,3) have "N`z∈⋃T" by auto moreover
        from n(2) z(1,2) have "N`z=⋃T" by auto ultimately
        have "False" using mem_not_refl by auto
      }
      then have reg:"∀n∈nat. ∃m∈nat. N`m≠⋃T ∧ ⟨n,m⟩∈Le" by auto
      let ?NN="{⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩. n∈nat}"
      {
        fix x z assume A1:"⟨x, z⟩ ∈ ?NN"
        {
          fix y' assume A2:"⟨x,y'⟩∈?NN"
          with A1 have "z=y'" by auto
        }
        then have "∀y'. ⟨x,y'⟩∈?NN ⟶ z=y'" by auto
      }
      then have "∀x z. ⟨x, z⟩ ∈ ?NN ⟶ (∀y'. ⟨x,y'⟩∈?NN ⟶ z=y')" by auto
      moreover
      {
        fix n assume as:"n∈nat"
        with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
        then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
          nat_into_Ord[of "m"] by auto
        then have "(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈nat" by auto
        then have "N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)∈⋃({one-point compactification of}T)" using apply_type[OF A(1)] op_compact_total by auto
        with as have "⟨n,N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)⟩∈nat×⋃({one-point compactification of}T)" by auto
      }
      then have "?NN∈Pow(nat×⋃({one-point compactification of}T))" by auto
      ultimately have NFun:"?NN:nat→⋃({one-point compactification of}T)" unfolding Pi_def function_def domain_def by auto
      {
        fix n assume as:"n∈nat"
        with reg obtain m where "N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m∈nat" by auto
        then have LI:"N`(μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le)≠⋃T" "⟨n,μ i. N`i≠⋃T ∧ ⟨n,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨n,m⟩∈Le" "m"]
          nat_into_Ord[of "m"] by auto
        then have "?NN`n≠⋃T" using apply_equality[OF _ NFun] by auto
      }
      then have noy:"∀n∈nat. ?NN`n≠⋃T" by auto
      then have "∀n∈nat. ?NN`n∈⋃T" using apply_type[OF NFun] op_compact_total by auto
      then have R:"?NN:nat→⋃T" using func1_1_L1A[OF NFun] by auto
      have dom2:"domain(?NN)=nat" by auto
      then have net2:"⟨?NN,Le⟩{is a net on}⋃T" unfolding IsNet_def using R dir by auto
      {
        fix U assume U:"U⊆⋃T" "x∈int(U)"
        have intT:"int(U)∈T" using Top_2_L2 by auto
        then have "int(U)∈({one-point compactification of}T)" unfolding OPCompactification_def
          by auto
        then have "Interior(int(U),{one-point compactification of}T)=int(U)" using topology0.Top_2_L3
          unfolding topology0_def using op_comp_is_top by auto
        with U(2) have "x∈Interior(int(U),{one-point compactification of}T)" by auto
        with intT have "(∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈int(U))" using comp op_compact_total by auto
        then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈U" using Top_2_L1 by auto
        {
          fix s assume AA:"⟨r,s⟩∈Le"
          with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
          then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
            nat_into_Ord by auto
          with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
          with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈U" by blast
          then have "?NN`s∈U" using apply_equality[OF _ NFun] AA by auto
        }
        then have "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
        with r_def(1) have "∃r∈nat. ∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈U" by auto
      }
      then have "∀U∈Pow(⋃T). x ∈ int(U)
        ⟶ (∃r∈nat. ∀s∈nat. ⟨r, s⟩ ∈ Le ⟶ ?NN ` s ∈ U)" by auto
      then have cony:"⟨?NN,Le⟩→⇩N x{in}T" using NetConverges_def[OF net2] x op_comp_is_top 
        unfolding topology0_def using xy(2) dom2 by auto
      let ?A="{x}∪?NN``nat"
      {
        fix M assume Acov:"?A⊆⋃M" "M⊆T"
        then have "x∈⋃M" by auto
        then obtain V where V:"x∈V" "V∈M" by auto
        with Acov(2) have VT:"V∈T" by auto
        then have "V=int(V)" using Top_2_L3 by auto
        with V(1) have "x∈int(V)" by auto
        with cony VT obtain r where rr:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ ?NN`s∈V"
          unfolding NetConverges_def[OF net2, of "x"] using dom2 y by auto
        have NresFun:"restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}):{n∈nat. ⟨n,r⟩∈Le}→⋃T" using restrict_fun
          [OF R, of "{n∈nat. ⟨n,r⟩∈Le}"] by auto
        then have "restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})∈surj({n∈nat. ⟨n,r⟩∈Le},range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le})))"
          using fun_is_surj by auto moreover
        have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
        then have "{n∈nat. ⟨n,r⟩∈Le}≲nat" using subset_imp_lepoll by auto
        ultimately have "range(restrict(?NN,{n∈nat. ⟨n,r⟩∈Le}))≲{n∈nat. ⟨n,r⟩∈Le}" using surj_fun_inv_2 by auto
        moreover
        have "{n∈nat. ⟨n,0⟩∈Le}={0}" by auto
        then have "Finite({n∈nat. ⟨n,0⟩∈Le})" by auto moreover
        {
          fix j assume as:"j∈nat" "Finite({n∈nat. ⟨n,j⟩∈Le})"
          {
            fix t assume "t∈{n∈nat. ⟨n,succ(j)⟩∈Le}"
            then have "t∈nat" "⟨t,succ(j)⟩∈Le" by auto
            then have "t≤succ(j)" by auto
            then have "t⊆succ(j)" using le_imp_subset by auto
            then have "t⊆j ∪{j}" using succ_explained by auto
            then have "j∈t∨t⊆j" by auto
            then have "j∈t∨t≤j" using subset_imp_le ‹t∈nat› ‹j∈nat› nat_into_Ord by auto
            then have "j ∪{j}⊆t∨t≤j" using ‹t∈nat› ‹j∈nat› nat_into_Ord unfolding Ord_def
              Transset_def by auto
            then have "succ(j)⊆t∨t≤j" using succ_explained by auto
            with ‹t⊆succ(j)› have "t=succ(j)∨t≤j" by auto
            with ‹t∈nat› ‹j∈nat› have "t∈{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
          }
          then have "{n∈nat. ⟨n,succ(j)⟩∈Le} ⊆{n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)}" by auto
          moreover have "Finite({n∈nat. ⟨n,j⟩∈Le} ∪ {succ(j)})" using as(2) Finite_cons
            by auto
          ultimately have "Finite({n∈nat. ⟨n,succ(j)⟩∈Le})" using subset_Finite by auto
        }
        then have "∀j∈nat. Finite({n∈nat. ⟨n,j⟩∈Le}) ⟶ Finite({n∈nat. ⟨n,succ(j)⟩∈Le})"
          by auto
        ultimately have "Finite(range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le})))"
          using lepoll_Finite[of "range(restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))"
            "{n ∈ nat . ⟨n, r⟩ ∈ Le}"] ind_on_nat[OF ‹r∈nat›, where P="λt. Finite({n∈nat. ⟨n,t⟩∈Le})"] by auto
        then have "Finite((restrict(?NN, {n ∈ nat . ⟨n, r⟩ ∈ Le}))``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using range_image_domain[OF NresFun]
          by auto
        then have "Finite(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})" using restrict_image by auto
        then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto
        moreover have "⋃(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})=⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
          unfolding RestrictedTo_def by auto moreover
        have "⋃T∩?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}=?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}"
          using func1_1_L6(2)[OF R] by blast
        moreover have "(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is a topology}"
          using Top_1_L4 unfolding topology0_def by auto
        ultimately have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T{restricted to}?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})"
          unfolding Spec_def by force
        then have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le}){is compact in}(T)" using compact_subspace_imp_compact by auto
        moreover from Acov(1) have "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃M" by auto
        moreover note Acov(2) ultimately
        obtain 𝔑 where 𝔑:"𝔑∈FinPow(M)" "(?NN``{n ∈ nat . ⟨n, r⟩ ∈ Le})⊆⋃𝔑"
          unfolding IsCompact_def by blast
        from 𝔑(1) have "𝔑 ∪{V}∈FinPow(M)" using V(2) unfolding FinPow_def by auto moreover
        {
          fix s assume s:"s∈?A" "s∉V"
          with V(1) have "s∈?NN``nat" by auto
          then have "s∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
          then obtain n where n:"n∈nat" "s=?NN`n" by auto
          {
            assume "⟨r,n⟩∈Le"
            with rr have "?NN`n∈V" by auto
            with n(2) s(2) have "False" by auto
          }
          then have "⟨r,n⟩∉Le" by auto
          with rr(1) n(1) have "¬(r≤n)" by auto
          then have "n≤r" using Ord_linear_le[where thesis="⟨n,r⟩∈Le"] nat_into_Ord[OF rr(1)]
            nat_into_Ord[OF n(1)] by auto
          with rr(1) n(1) have "⟨n,r⟩∈Le" by auto
          with n(2) have "s∈{?NN`t. t∈{n∈nat. ⟨n,r⟩∈Le}}" by auto moreover
          have "{n∈nat. ⟨n,r⟩∈Le}⊆nat" by auto
          ultimately have "s∈?NN``{n∈nat. ⟨n,r⟩∈Le}" using func_imagedef[OF NFun]
            by auto
          with 𝔑(2) have "s∈⋃𝔑" by auto
        }
        then have "?A⊆⋃𝔑 ∪ V" by auto
        then have "?A⊆⋃(𝔑 ∪ {V})" by auto ultimately
        have "∃𝔑∈FinPow(M). ?A⊆⋃𝔑" by auto
      }
      then have "∀M∈Pow(T). ?A⊆⋃M ⟶ (∃𝔑∈FinPow(M). ?A⊆⋃𝔑)" by auto moreover
      have ss:"?A⊆⋃(T)" using func1_1_L6(2)[OF R] x by blast ultimately
      have "?A{is compact in}(T)" unfolding IsCompact_def by auto moreover
      with assms have "?A{is closed in}(T)" unfolding IsKC_def IsCompact_def by auto ultimately
      have "?A∈{B∈Pow(⋃T). B{is compact in}(T)∧B{is closed in}(T)}" using ss by auto
      then have "{⋃T}∪(⋃T-?A)∈({one-point compactification of}T)" unfolding OPCompactification_def
        by auto
      then have "{⋃T}∪(⋃T-?A)=Interior({⋃T}∪(⋃T-?A),{one-point compactification of}T)" using topology0.Top_2_L3 op_comp_is_top
        unfolding topology0_def by auto moreover
      {
        assume "y∈?A"
        with A(4) have "y∈?NN``nat" by auto
        then have "y∈{?NN`n. n∈nat}" using func_imagedef[OF NFun] by auto
        then obtain n where "n∈nat""?NN`n=y" by auto
        with noy y have "False" by auto
      }
      with y have "y∈{⋃T}∪(⋃T-?A)" by force ultimately
      have "y∈Interior({⋃T}∪(⋃T-?A),{one-point compactification of}T)" "{⋃T}∪(⋃T-?A)∈Pow(⋃({one-point compactification of}T))"
        using op_compact_total by auto moreover
      have "(∀U∈Pow(⋃({one-point compactification of}T)). y ∈ Interior(U,{one-point compactification of}T) ⟶ (∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ U))"
        using A(3) dom topology0.NetConverges_def[OF _ NET] op_comp_is_top unfolding topology0_def by auto
      ultimately have "∃t∈nat. ∀m∈nat. ⟨t, m⟩ ∈ Le ⟶ N ` m ∈ {⋃T}∪(⋃T-?A)" by blast
      then obtain r where r_def:"r∈nat" "∀s∈nat. ⟨r,s⟩∈Le ⟶ N`s∈{⋃T}∪(⋃T-?A)" by auto
      {
        fix s assume AA:"⟨r,s⟩∈Le"
        with reg obtain m where "N`m≠⋃T" "⟨s,m⟩∈Le" by auto
        then have "⟨s,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using LeastI[of "λm. N`m≠⋃T ∧ ⟨s,m⟩∈Le" "m"]
          nat_into_Ord by auto
        with AA have "⟨r,μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le⟩∈Le" using le_trans by auto
        with r_def(2) have "N`(μ i. N`i≠⋃T ∧ ⟨s,i⟩∈Le)∈{⋃T}∪(⋃T-?A)" by auto
        then have "?NN`s∈{⋃T}∪(⋃T-?A)" using apply_equality[OF _ NFun] AA by auto
        with noy have "?NN`s∈(⋃T-?A)" using AA by auto
        moreover have "?NN`s∈{?NN`t. t∈nat}" using AA by auto
        then have "?NN`s∈?NN``nat" using func_imagedef[OF NFun] by auto
        then have "?NN`s∈?A" by auto
        ultimately have "False" by auto
      }
      moreover have "r⊆succ(r)" using succ_explained by auto
      then have "r≤succ(r)" using subset_imp_le nat_into_Ord ‹r∈nat› nat_succI
        by auto
      then have "⟨r,succ(r)⟩∈Le" using ‹r∈nat› nat_succI by auto
      ultimately have "False" by auto
    }
    ultimately have "False" by auto
  }
  then have "∀N x y. N:nat→(⋃{one-point compactification of}T) ∧ (⟨N,Le⟩→⇩N x{in}({one-point compactification of}T))
    ∧ (⟨N,Le⟩→⇩N y{in}({one-point compactification of}T)) ⟶ x=y" by auto
  then show ?thesis unfolding IsUS_def by auto
qed

text‹In the one-point compactification of an anti-compact space,
ever subspace that contains the infinite point is compact.›

theorem (in topology0) anti_comp_imp_OP_inf_comp:
  assumes "T{is anti-compact}" "A⊆⋃({one-point compactification of}T)" "⋃T∈A"
  shows "A{is compact in}({one-point compactification of}T)"
proof-
  {
    fix M assume M:"M⊆({one-point compactification of}T)" "A⊆⋃M"
    with assms(3) obtain U where U:"⋃T∈U" "U∈M" by auto
    with M(1) obtain K where K:"K{is compact in}T" "K{is closed in}T" "U={⋃T}∪(⋃T-K)"
      unfolding OPCompactification_def using mem_not_refl[of "⋃T"] by auto
    from K(1) have "K{is compact in}(T{restricted to}K)" using compact_imp_compact_subspace Compact_is_card_nat
      by auto
    moreover have "⋃(T{restricted to}K)=⋃T∩K" unfolding RestrictedTo_def by auto
    with K(1) have "⋃(T{restricted to}K)=K" unfolding IsCompact_def by auto ultimately
    have "(⋃(T{restricted to}K)){is compact in}(T{restricted to}K)" by auto
    with assms(1) have "K{is in the spectrum of}(λT. (⋃T){is compact in}T)" unfolding IsAntiComp_def
      antiProperty_def using K(1) unfolding IsCompact_def by auto
    then have finK:"Finite(K)" using compact_spectrum by auto
    from assms(2) have "A-U⊆(⋃T ∪{⋃T}) -U" using op_compact_total by auto
    with K(3) have "A-U⊆K" by auto
    with finK have "Finite(A-U)" using subset_Finite by auto
    then have "(A-U){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum by auto moreover
    have "⋃(({one-point compactification of}T){restricted to}(A-U))=A-U" unfolding RestrictedTo_def using assms(2) K(3)
      op_compact_total by auto moreover
    have "(({one-point compactification of}T){restricted to}(A-U)){is a topology}" using topology0.Top_1_L4
      op_comp_is_top unfolding topology0_def by auto
    ultimately have "(A-U){is compact in}(({one-point compactification of}T){restricted to}(A-U))"
      unfolding Spec_def by auto
    then have "(A-U){is compact in}({one-point compactification of}T)" using compact_subspace_imp_compact by auto
    moreover have "A-U⊆⋃M" using M(2) by auto moreover
    note M(1) ultimately obtain N where N:"N∈FinPow(M)" "A-U⊆⋃N" unfolding IsCompact_def by blast
    from N(1) U(2) have "N ∪{U}∈FinPow(M)" unfolding FinPow_def by auto moreover
    from N(2) have "A⊆⋃(N ∪{U})" by auto
    ultimately have "∃R∈FinPow(M). A⊆⋃R" by auto
  }
  then show ?thesis using op_compact_total assms(2) unfolding IsCompact_def by auto
qed

text‹As a last result in this section, the one-point compactification of our topology is not a KC space.›

theorem extension_pow_OP_not_KC:
  shows "¬(({one-point compactification of}(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})){is KC})"
proof
  have noE:"csucc(nat)≠0" using Ord_0_lt_csucc[OF Ord_nat] by auto
  let ?T="(Pow(csucc(nat)) ∪ {{csucc(nat)}∪S. S∈(CoCountable csucc(nat))-{0}})"
  assume ass:"({one-point compactification of}?T){is KC}"
  from extension_pow_notDiscrete have "{csucc(nat)} ∉ (Pow(csucc(nat)) ∪ {{csucc(nat)} ∪ S . S ∈ (CoCountable csucc(nat)) - {0}})"
    by auto
  {
    assume "csucc(nat)=csucc(nat)∪{csucc(nat)}" moreover
    have "csucc(nat)∈csucc(nat)∪{csucc(nat)}" by auto
    ultimately have "csucc(nat)∈csucc(nat)" by auto
    then have "False" using mem_not_refl by auto
  }
  then have dist:"csucc(nat)≠csucc(nat)∪{csucc(nat)}" by blast
  {
    assume "{csucc(nat)}∈({one-point compactification of}(Pow(csucc(nat)) ∪ {{csucc(nat)} ∪ S . S ∈ (CoCountable csucc(nat)) - {0}}))"
    then have "{csucc(nat)}∈{{⋃?T}∪((⋃?T)-K). K∈{B∈Pow(⋃?T). B{is compact in}?T ∧ B{is closed in}?T}}"
      unfolding OPCompactification_def using extension_pow_notDiscrete by auto
    then obtain K where "{csucc(nat)}={⋃?T}∪((⋃?T)-K)" by auto moreover
    have "⋃?T∈{⋃?T}∪((⋃?T)-K)" by auto
    ultimately have "⋃?T∈{csucc(nat)}" by auto
    with dist have "False" using extension_pow_union by auto
  }
  then have "{csucc(nat)}∉({one-point compactification of}?T)" by auto moreover
  have "⋃({one-point compactification of}?T)-(⋃({one-point compactification of}?T)-{csucc(nat)})={csucc(nat)}" using extension_pow_union
    topology0.op_compact_total unfolding topology0_def using extension_pow_top by auto ultimately
  have di:"⋃({one-point compactification of}?T)-(⋃({one-point compactification of}?T)-{csucc(nat)})∉({one-point compactification of}?T)" by auto
  {
    assume "(⋃({one-point compactification of}?T)-{csucc(nat)}){is closed in}({one-point compactification of}?T)"
    then have "⋃({one-point compactification of}?T)-(⋃({one-point compactification of}?T)-{csucc(nat)})∈({one-point compactification of}?T)" unfolding IsClosed_def by auto
    with di have "False" by auto
  }
  then have n:"¬((⋃({one-point compactification of}?T)-{csucc(nat)}){is closed in}({one-point compactification of}?T))" by auto moreover
  from dist have "⋃?T∈(⋃({one-point compactification of}?T)-{csucc(nat)})" using topology0.op_compact_total unfolding topology0_def using extension_pow_top
    extension_pow_union by auto
  then have "(⋃({one-point compactification of}?T)-{csucc(nat)}){is compact in}({one-point compactification of}?T)" using topology0.anti_comp_imp_OP_inf_comp[of "?T"
    "(⋃({one-point compactification of}?T)-{csucc(nat)})"] unfolding topology0_def using extension_pow_antiCompact extension_pow_top by auto
  with ass have "(⋃({one-point compactification of}?T)-{csucc(nat)}){is closed in}({one-point compactification of}?T)" unfolding IsKC_def by auto
  with n show "False" by auto
qed
    
text‹In conclusion, $US\not\Rightarrow KC$.›

subsection‹Other types of properties›

text‹In this section we will define new properties that
aren't defined as anti-properties and that are not separation axioms.
In some cases we will consider their anti-properties.›

subsection‹Definitions›

text‹A space is called perfect if it has no isolated points.
This definition may vary in the literature to similar, but not equivalent definitions.›

definition
  IsPerf ("_ {is perfect}") where
  "T{is perfect} ≡ ∀x∈⋃T. {x}∉T"

text‹An anti-perfect space is called scattered.›

definition
  IsScatt ("_ {is scattered}") where
  "T{is scattered} ≡ T{is anti-}IsPerf"

text‹A topological space with two disjoint dense subspaces
is called resolvable.›

definition
  IsRes ("_ {is resolvable}") where
  "T{is resolvable} ≡ ∃U∈Pow(⋃T). ∃V∈Pow(⋃T). Closure(U,T)=⋃T ∧ Closure(V,T)=⋃T ∧ U∩V=0"

text‹A topological space where every dense subset is open
is called submaximal.›

definition
  IsSubMax ("_ {is submaximal}") where
  "T{is submaximal} ≡ ∀U∈Pow(⋃T). Closure(U,T)=⋃T ⟶ U∈T"

text‹A subset of a topological space is nowhere-dense if
the interior of its closure is empty.›

definition
  IsNowhereDense ("_ {is nowhere dense in} _") where
  "A{is nowhere dense in}T ≡ A⊆⋃T ∧ Interior(Closure(A,T),T)=0"

text‹A topological space is then a Luzin space if
every nowhere-dense subset is countable.›

definition
  IsLuzin ("_ {is luzin}") where
  "T{is luzin} ≡ ∀A∈Pow(⋃T). (A{is nowhere dense in}T) ⟶ A≲nat"

text‹An also useful property is local-connexion.›

definition
  IsLocConn ("_{is locally-connected}") where
  "T{is locally-connected} ≡ T{is locally}(λT. λB. ((T{restricted to}B){is connected}))"

text‹An SI-space is an anti-resolvable perfect space.›

definition
  IsAntiRes ("_{is anti-resolvable}") where
  "T{is anti-resolvable} ≡ T{is anti-}IsRes"

definition
  IsSI ("_{is Strongly Irresolvable}") where
  "T{is Strongly Irresolvable} ≡ (T{is anti-resolvable}) ∧ (T{is perfect})"

subsection‹First examples›

text‹Firstly, we need to compute the spectrum of
the being perfect.›

lemma spectrum_perfect:
  shows "(A{is in the spectrum of}IsPerf) ⟷ A=0"
proof
  assume "A{is in the spectrum of}IsPerf"
  then have "Pow(A){is perfect}" unfolding Spec_def using Pow_is_top by auto
  then have "∀b∈A. {b}∉Pow(A)" unfolding IsPerf_def by auto
  then show "A=0" by auto
next
  assume A:"A=0"
  {
    fix T assume T:"T{is a topology}" "⋃T≈A"
    with T(2) A have "⋃T≈0" by auto
    then have "⋃T=0" using eqpoll_0_is_0 by auto
    then have "T{is perfect}" unfolding IsPerf_def by auto
  }
  then show "A{is in the spectrum of}IsPerf" unfolding Spec_def by auto
qed

text‹The discrete space is clearly scattered:›

lemma pow_is_scattered:
  shows "Pow(A){is scattered}"
proof-
  {
    fix B assume B:"B⊆⋃Pow(A)" "(Pow(A){restricted to}B){is perfect}"
    from B(1) have "Pow(A){restricted to}B=Pow(B)" unfolding RestrictedTo_def by blast
    with B(2) have "Pow(B){is perfect}" by auto
    then have "∀b∈B. {b}∉Pow(B)" unfolding IsPerf_def by auto
    then have "B=0" by auto
  }
  then show ?thesis using spectrum_perfect unfolding IsScatt_def antiProperty_def by auto
qed

text‹The trivial topology is perfect, if it is defined over a set with more than one point.›

lemma trivial_is_perfect:
  assumes "∃x y. x∈X ∧ y∈X ∧ x≠y"
  shows "{0,X}{is perfect}"
proof-
  {
    fix r assume "{r}∈{0,X}"
    then have "X={r}" by auto
    with assms have "False" by auto
  }
  then show ?thesis unfolding IsPerf_def by auto
qed

text‹The trivial topology is resolvable, if it is defined over a set with more than one point.›

lemma trivial_is_resolvable:
  assumes "∃x y. x∈X ∧ y∈X ∧ x≠y"
  shows "{0,X}{is resolvable}"
proof-
  from assms obtain x y where xy:"x∈X" "y∈X" "x≠y" by auto
  {
    fix A assume A:"A{is closed in}{0,X}" "A⊆X"
    then have "X-A∈{0,X}" unfolding IsClosed_def by auto
    then have "X-A=0∨X-A=X" by auto
    with A(2) have "A=X∨X-A=X" by auto moreover
    {
      assume "X-A=X"
      then have "X-(X-A)=0" by auto
      with A(2) have "A=0" by auto
    }
    ultimately have "A=X∨A=0" by auto
    then have "A=0∨A=X" by auto
  }
  then have cl:"∀A∈Pow(X). A{is closed in}{0,X} ⟶ A=0∨A=X" by auto
  from xy(3) have "{x}∩{y}=0" by auto moreover
  {
    have "{X}{is a partition of}X" using indiscrete_partition xy(1) by auto
    then have top:"topology0(PTopology X {X})" using topology0_ptopology by auto
    have "X≠0" using xy(1) by auto
    then have "(PTopology X {X})={0,X}" using indiscrete_ptopology[of "X"] by auto
    with top have top0:"topology0({0,X})" by auto
    then have "x∈Closure({x},{0,X})" using topology0.cl_contains_set xy(1) by auto moreover
    have "Closure({x},{0,X}) {is closed in}{0,X}" using topology0.cl_is_closed top0 xy(1) by auto
    moreover note cl
    moreover have "Closure({x},{0,X})⊆X" using topology0.Top_3_L11(1) top0 xy(1) by auto
    ultimately have "Closure({x},{0,X})=X" by auto
  }
  moreover
  {
    have "{X}{is a partition of}X" using indiscrete_partition xy(1) by auto
    then have top:"topology0(PTopology X {X})" using topology0_ptopology by auto
    have "X≠0" using xy(1) by auto
    then have "(PTopology X {X})={0,X}" using indiscrete_ptopology[of "X"] by auto
    with top have top0:"topology0({0,X})" by auto
    then have "y∈Closure({y},{0,X})" using topology0.cl_contains_set xy(2) by auto moreover
    have "Closure({y},{0,X}) {is closed in}{0,X}" using topology0.cl_is_closed top0 xy(2) by auto
    moreover note cl
    moreover have "Closure({y},{0,X})⊆X" using topology0.Top_3_L11(1) top0 xy(2) by auto
    ultimately have "Closure({y},{0,X})=X" by auto
  } 
  ultimately show ?thesis using xy(1,2) unfolding IsRes_def by auto
qed

text‹The spectrum of Luzin spaces is the class of countable sets, so there
are lots of examples of Luzin spaces.›

lemma spectrum_Luzin:
  shows "(A{is in the spectrum of}IsLuzin) ⟷ A≲nat"
proof
  assume A:"A{is in the spectrum of}IsLuzin"
  {
    assume "A=0"
    then have "A≲nat" using empty_lepollI by auto
  }
  moreover
  {
    assume "A≠0"
    then obtain x where x:"x∈A" by auto
    {
      fix M assume "M⊆{0,{x},A}"
      then have "⋃M∈{0,{x},A}" using x by blast
    }
    moreover
    {
      fix U V assume "U∈{0,{x},A}" "V∈{0,{x},A}"
      then have "U∩V∈{0,{x},A}" by auto
    }
    ultimately have top:"{0,{x},A}{is a topology}" unfolding IsATopology_def by auto
    moreover have tot:"⋃{0,{x},A}=A" using x by auto
    moreover note A ultimately have luz:"{0,{x},A}{is luzin}" unfolding Spec_def by auto
    moreover have "{x}∈{0,{x},A}" by auto
    then have "((⋃{0,{x},A})-{x}){is closed in}{0,{x},A}" using topology0.Top_3_L9
      unfolding topology0_def using top by blast
    then have "(A-{x}){is closed in}{0,{x},A}" using tot by auto
    then have "Closure(A-{x},{0,{x},A})=A-{x}" using tot top topology0.Top_3_L8[of "{0,{x},A}"]
      unfolding topology0_def by auto
    then have B:"Interior(Closure(A-{x},{0,{x},A}),{0,{x},A})=Interior(A-{x},{0,{x},A})" by auto
    then have C:"Interior(Closure(A-{x},{0,{x},A}),{0,{x},A})⊆A-{x}" using top topology0.Top_2_L1
      unfolding topology0_def by auto
    then have D:"Interior(Closure(A-{x},{0,{x},A}),{0,{x},A})∈{0,{x},A}" using topology0.Top_2_L2 
      unfolding topology0_def using top by auto
    from x have "¬(A⊆A-{x})" by auto
    with C D have "Interior(Closure(A-{x},{0,{x},A}),{0,{x},A})=0" by auto
    then have "(A-{x}){is nowhere dense in}{0,{x},A}" unfolding IsNowhereDense_def using tot
      by auto
    with luz have "A-{x}≲nat" unfolding IsLuzin_def using tot by auto
    then have U1:"A-{x}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
    have "{x}≈1" using singleton_eqpoll_1 by auto
    then have "{x}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto
    then have "{x}≲nat" using lesspoll_imp_lepoll by auto
    then have U2:"{x}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
    with U1 have U:"(A-{x})∪{x}≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]]
      by auto
    have "(A-{x})∪{x}=A" using x by auto
    with U have "A≺csucc(nat)" by auto
    then have "A≲nat" using Card_less_csucc_eq_le[OF Card_nat] by auto
  }
  ultimately
  show "A≲nat" by auto
next
  assume A:"A≲nat"
  {
    fix T assume T:"T{is a topology}" "⋃T≈A"
    {
      fix B assume "B⊆⋃T" "B{is nowhere dense in}T"
      then have "B≲⋃T" using subset_imp_lepoll by auto
      with T(2) have "B≲A" using lepoll_eq_trans by auto
      with A have "B≲nat" using lepoll_trans by blast
    }
    then have "∀B∈Pow(⋃T). (B{is nowhere dense in}T) ⟶ B≲nat" by auto
    then have "T{is luzin}" unfolding IsLuzin_def by auto
  }
  then show "A{is in the spectrum of}IsLuzin" unfolding Spec_def by auto
qed

subsection‹Structural results›

text‹Every resolvable space is also perfect.›

theorem (in topology0) resolvable_imp_perfect:
  assumes "T{is resolvable}"
  shows "T{is perfect}"
proof-
  {
    assume "¬(T{is perfect})"
    then obtain x where x:"x∈⋃T" "{x}∈T" unfolding IsPerf_def by auto
    then have cl:"(⋃T-{x}){is closed in}T" using Top_3_L9 by auto
    from assms obtain U V where UV:"U⊆⋃T" "V⊆⋃T" "cl(U)=⋃T" "cl(V)=⋃T" "U∩V=0" unfolding IsRes_def by auto
    {
      fix W assume "x∉W" "W⊆⋃T"
      then have "W⊆⋃T-{x}" by auto
      then have "cl(W)⊆⋃T-{x}" using cl Top_3_L13 by auto
      with x(1) have "¬(⋃T⊆cl(W))" by auto
      then have "¬(cl(W)=⋃T)" by auto
    }
    with UV have "False" by auto
  }
  then show ?thesis by auto
qed
   
text‹The spectrum of being resolvable follows:›

corollary spectrum_resolvable:
  shows "(A{is in the spectrum of}IsRes) ⟷ A=0"
proof
  assume A:"A{is in the spectrum of}IsRes"
  have "∀T. T{is a topology} ⟶ IsRes(T) ⟶ IsPerf(T)" using topology0.resolvable_imp_perfect 
    unfolding topology0_def by auto
  with A have "A{is in the spectrum of}IsPerf" using P_imp_Q_spec_inv[of IsRes IsPerf] by auto
  then show "A=0" using spectrum_perfect by auto
next
  assume A:"A=0"
  {
    fix T assume T:"T{is a topology}" "⋃T≈A"
    with T(2) A have "⋃T≈0" by auto
    then have "⋃T=0" using eqpoll_0_is_0 by auto
    then have "Closure(0,T)=⋃T" using topology0.Top_3_L2 T(1)
      topology0.Top_3_L8 unfolding topology0_def by auto
    then have "T{is resolvable}" unfolding IsRes_def by auto
  }
  then show "A{is in the spectrum of}IsRes" unfolding Spec_def by auto
qed

text‹The cofinite space over $\mathbb{N}$ is a $T_1$, perfect and luzin space.›

theorem cofinite_nat_perfect:
  shows "(CoFinite nat){is perfect}"
proof-
  {
    fix x assume x:"x∈⋃(CoFinite nat)" "{x}∈(CoFinite nat)"
    then have xn:"x∈nat" using union_cocardinal unfolding Cofinite_def by auto
    with x(2) have "nat-{x}≺nat" unfolding Cofinite_def CoCardinal_def by auto
    moreover have "Finite({x})" by auto
    then have "{x}≺nat" unfolding Finite_def using n_lesspoll_nat eq_lesspoll_trans by auto
    ultimately have "(nat-{x})∪{x}≺nat" using less_less_imp_un_less[OF _ _ InfCard_nat] by auto
    moreover have "(nat-{x})∪{x}=nat" using xn by auto
    ultimately have "False" by auto
  }
  then show ?thesis unfolding IsPerf_def by auto
qed

theorem cofinite_nat_luzin:
  shows "(CoFinite nat){is luzin}"
proof-
  have "nat{is in the spectrum of}IsLuzin" using spectrum_Luzin by auto moreover
  have "⋃(CoFinite nat)=nat" using union_cocardinal unfolding Cofinite_def by auto
  moreover have "(CoFinite nat){is a topology}" unfolding Cofinite_def using CoCar_is_topology[OF InfCard_nat]
    by auto
  ultimately show ?thesis unfolding Spec_def by auto
qed

text‹The cocountable topology on $\mathbb{N}^+$ or ‹csucc(nat)› is also $T_1$,
perfect and luzin; but defined on a set not in the spectrum.›

theorem cocountable_csucc_nat_perfect:
  shows "(CoCountable csucc(nat)){is perfect}"
proof-
  have noE:"csucc(nat)≠0" using lt_csucc[OF Ord_nat] by auto 
  {
    fix x assume x:"x∈⋃(CoCountable csucc(nat))" "{x}∈(CoCountable csucc(nat))"
    then have xn:"x∈csucc(nat)" using union_cocardinal noE unfolding Cocountable_def by auto
    with x(2) have "csucc(nat)-{x}≺csucc(nat)" unfolding Cocountable_def CoCardinal_def by auto
    moreover have "Finite({x})" by auto
    then have "{x}≺nat" unfolding Finite_def using n_lesspoll_nat eq_lesspoll_trans by auto
    then have "{x}≲nat" using lesspoll_imp_lepoll by auto
    then have "{x}≺csucc(nat)" using Card_less_csucc_eq_le[OF Card_nat] by auto
    ultimately have "(csucc(nat)-{x})∪{x}≺csucc(nat)" using less_less_imp_un_less[OF _ _ InfCard_csucc[OF InfCard_nat]] by auto
    moreover have "(csucc(nat)-{x})∪{x}=csucc(nat)" using xn by auto
    ultimately have "False" by auto
  }
  then show ?thesis unfolding IsPerf_def by auto
qed

theorem cocountable_csucc_nat_luzin:
  shows "(CoCountable csucc(nat)){is luzin}"
proof-
  have noE:"csucc(nat)≠0" using lt_csucc[OF Ord_nat] by auto 
  {
    fix B assume B:"B∈Pow(⋃(CoCountable csucc(nat)))" "B{is nowhere dense in}(CoCountable csucc(nat))" "¬(B≲nat)"
    from B(1) have "B⊆csucc(nat)" using union_cocardinal noE unfolding Cocountable_def by auto moreover
    from B(3) have "¬(B≺csucc(nat))" using Card_less_csucc_eq_le[OF Card_nat] by auto ultimately
    have "Closure(B,CoCountable csucc(nat))=csucc(nat)" using closure_set_cocardinal noE unfolding Cocountable_def by auto
    then have "Interior(Closure(B,CoCountable csucc(nat)),CoCountable csucc(nat))=Interior(csucc(nat),CoCountable csucc(nat))" by auto
    with B(2) have "0=Interior(csucc(nat),CoCountable csucc(nat))" unfolding IsNowhereDense_def by auto moreover
    have "csucc(nat)-csucc(nat)=0" by auto
    then have "csucc(nat)-csucc(nat)≺csucc(nat)" using empty_lepollI Card_less_csucc_eq_le[OF Card_nat] by auto
    then have "Interior(csucc(nat),CoCountable csucc(nat))=csucc(nat)" using interior_set_cocardinal noE unfolding Cocountable_def by auto
    ultimately have "False" using noE by auto
  }
  then have "∀B∈Pow(⋃(CoCountable csucc(nat))). (B{is nowhere dense in}(CoCountable csucc(nat))) ⟶ B≲nat" by auto
  then show ?thesis unfolding IsLuzin_def by auto
qed

text‹The existence of $T_2$, uncountable, perfect and luzin spaces is unprovable in \emph{ZFC}.
It is related to the \emph{CH} and Martin's axiom.›

end