Theory Topology_ZF_properties_2

(* 
    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 2›

theory Topology_ZF_properties_2 imports Topology_ZF_7 Topology_ZF_1b
  Finite_ZF_1 Topology_ZF_11

begin

subsection‹Local properties.›
text‹This theory file deals with local topological properties; and applies local compactness
to the one point compactification.›

text‹We will say that a topological space is locally @term{"P"} iff every point has a neighbourhood basis
of subsets that have the property @term{"P"} as subspaces.›

definition
  IsLocally ("_{is locally}_" 90)
  where "T{is a topology} ⟹ T{is locally}P ≡ (∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,T) ∧ P(c,T)))"

subsection‹First examples›
text‹Our first examples deal with the locally finite property. Finiteness is a property of sets,
and hence it is preserved by homeomorphisms; which are in particular bijective.›

text‹The discrete topology is locally finite.›

lemma discrete_locally_finite:
  shows "Pow(A){is locally}(λA.(λB. Finite(A)))"
proof-
  have "∀b∈Pow(A). ⋃(Pow(A){restricted to}b)=b" unfolding RestrictedTo_def by blast
  then have "∀b∈{{x}. x∈A}. Finite(b)" by auto moreover
  have reg:"∀S∈Pow(A). Interior(S,Pow(A))=S" unfolding Interior_def by auto
  {
    fix x b assume "x∈⋃Pow(A)" "b∈Pow(A)" "x∈b"
    then have "{x}⊆b" "x∈Interior({x},Pow(A))" "Finite({x})" using reg by auto
    then have "∃c∈Pow(b). x∈Interior(c,Pow(A))∧Finite(c)" by blast
  }
  then have "∀x∈⋃Pow(A). ∀b∈Pow(A). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,Pow(A)) ∧ Finite(c))" by auto
  then show ?thesis using IsLocally_def[OF Pow_is_top] by auto
qed

text‹The included set topology is locally finite when the set is finite.›

lemma included_finite_locally_finite:
  assumes "Finite(A)" and "A⊆X"
  shows "(IncludedSet(X,A)){is locally}(λA.(λB. Finite(A)))"
proof-
  have "∀b∈Pow(X). b∩A⊆b" by auto moreover
  note assms(1)
  ultimately have rr:"∀b∈{A∪{x}. x∈X}. Finite(b)" by force
  {
    fix x b assume "x∈⋃(IncludedSet(X,A))" "b∈(IncludedSet(X,A))" "x∈b"
    then have "A∪{x}⊆b" "A∪{x}∈{A∪{x}. x∈X}" and sub: "b⊆X" unfolding IncludedSet_def by auto
    moreover have "A ∪ {x} ⊆ X" using assms(2) sub ‹x∈b› by auto
    then have "x∈Interior(A∪{x},IncludedSet(X,A))" using interior_set_includedset[of "A∪{x}""X""A"] by auto
    ultimately have "∃c∈Pow(b). x∈Interior(c,IncludedSet(X,A))∧ Finite(c)" using rr by blast
  }
  then have "∀x∈⋃(IncludedSet(X,A)). ∀b∈(IncludedSet(X,A)). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,IncludedSet(X,A))∧ Finite(c))" by auto
  then show ?thesis using IsLocally_def includedset_is_topology by auto
qed

subsection‹Local compactness›

definition
  IsLocallyComp ("_{is locally-compact}" 70)
  where "T{is locally-compact}≡T{is locally}(λB. λT. B{is compact in}T)"

text‹We center ourselves in local compactness, because it is a very important tool in topological groups
and compactifications.›

text‹If a subset is compact of some cardinal for a topological space, it is compact of the same cardinal
in the subspace topology.›

lemma compact_imp_compact_subspace:
  assumes "A{is compact of cardinal}K{in}T" "A⊆B"
  shows "A{is compact of cardinal}K{in}(T{restricted to}B)" unfolding IsCompactOfCard_def
proof
  from assms show C:"Card(K)" unfolding IsCompactOfCard_def by auto
  from assms have "A⊆⋃T" unfolding IsCompactOfCard_def by auto
  then have AA:"A⊆⋃(T{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto moreover
  {
    fix M assume "M∈Pow(T{restricted to}B)" "A⊆⋃M"
    let ?M="{S∈T. B∩S∈M}"
    from ‹M∈Pow(T{restricted to}B)› have "⋃M⊆⋃?M" unfolding RestrictedTo_def by auto
    with ‹A⊆⋃M› have "A⊆⋃?M""?M∈Pow(T)" by auto
    with assms have "∃N∈Pow(?M). A⊆⋃N∧N≺K" unfolding IsCompactOfCard_def by auto
    then obtain N where "N∈Pow(?M)" "A⊆⋃N" "N≺K" by auto
    then have "N{restricted to}B⊆M" unfolding RestrictedTo_def FinPow_def by auto
    moreover
    let ?f="{⟨𝔅,B∩𝔅⟩. 𝔅∈N}"
    have "?f:N→(N{restricted to}B)" unfolding Pi_def function_def domain_def RestrictedTo_def by auto
    then have "?f∈surj(N,N{restricted to}B)" unfolding surj_def RestrictedTo_def using apply_equality
      by auto
    from ‹N≺K› have "N≲K" unfolding lesspoll_def by auto
    with ‹?f∈surj(N,N{restricted to}B)› have "N{restricted to}B≲N" using surj_fun_inv_2 Card_is_Ord C by auto
    with ‹N≺K› have "N{restricted to}B≺K" using lesspoll_trans1 by auto
    moreover from ‹A⊆⋃N› have "A⊆⋃(N{restricted to}B)" using assms(2) unfolding RestrictedTo_def by auto
    ultimately have "∃N∈Pow(M). A⊆⋃N ∧ N≺K" by auto
  }
  with AA show "A ⊆ ⋃(T {restricted to} B) ∧ (∀M∈Pow(T {restricted to} B). A ⊆ ⋃M ⟶ (∃N∈Pow(M). A ⊆ ⋃N ∧ N≺K))" by auto
qed

text‹The converse of the previous result is not always true. For compactness, it holds because the axiom of finite choice
always holds.›

lemma compact_subspace_imp_compact:
  assumes "A{is compact in}(T{restricted to}B)" "A⊆B"
  shows "A{is compact in}T" unfolding IsCompact_def
proof
  from assms show "A⊆⋃T" unfolding IsCompact_def RestrictedTo_def by auto
next
  {
    fix M assume "M∈Pow(T)" "A⊆⋃M"
    let ?M="M{restricted to}B"
    from ‹M∈Pow(T)› have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto
    from ‹A⊆⋃M› have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto
    with assms ‹?M∈Pow(T{restricted to}B)› obtain N where "N∈FinPow(?M)" "A⊆⋃N" unfolding IsCompact_def by blast
    from ‹N∈FinPow(?M)› have "N≺nat" unfolding FinPow_def Finite_def using n_lesspoll_nat eq_lesspoll_trans
      by auto
    then have "Finite(N)" using lesspoll_nat_is_Finite by auto
    then obtain n where "n∈nat" "N≈n" unfolding Finite_def by auto
    then have "N≲n" using eqpoll_imp_lepoll by auto
    moreover 
    {
      fix BB assume "BB∈N"
      with ‹N∈FinPow(?M)› have "BB∈?M" unfolding FinPow_def by auto
      then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto
      then have "S∈{S∈M. B∩S=BB}" by auto
      then obtain "{S∈M. B∩S=BB}≠0" by auto
    }
    then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover
    from ‹n∈nat› have " (N ≲ n ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))" using finite_choice unfolding AxiomCardinalChoiceGen_def by blast
    ultimately
    obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast
    from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto
    then have "{f`t. t∈N}⊆M" by auto
    {
      fix t assume "t∈N"
      with ss have "f`t∈{S∈M. B∩S∈N}" by auto
    }
    with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover
    {
      fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb"
      from AAA(1) ss have "B∩ (f`aa) =aa" by auto
      with AAA(3) have "B∩(f`bb)=aa" by auto
      with ss AAA(2) have "aa=bb" by auto
    }
    ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto
    then have "f∈bij(N,range(f))" using inj_bij_range by auto
    then have "f∈bij(N,f``N)" using range_image_domain FF by auto
    then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto
    then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto
    with ‹N≈n› have "{f`t. t∈N}≈n" using eqpoll_sym eqpoll_trans by blast
    with ‹n∈nat› have "Finite({f`t. t∈N})" unfolding Finite_def by auto
    with ss have "{f`t. t∈N}∈FinPow(M)" unfolding FinPow_def by auto moreover
    {
      fix aa assume "aa∈A"
      with ‹A⊆⋃N› obtain b where "b∈N" and "aa∈b" by auto
      with ss have "B∩(f`b)=b" by auto
      with ‹aa∈b› have "aa∈B∩(f`b)" by auto
      then have "aa∈ f`b" by auto
      with ‹b∈N› have "aa∈⋃{f`t. t∈N}" by auto
    }
    then have "A⊆⋃{f`t. t∈N}" by auto ultimately
    have "∃R∈FinPow(M). A⊆⋃R" by auto
  }
  then show "∀M∈Pow(T). A ⊆ ⋃M ⟶ (∃N∈FinPow(M). A ⊆ ⋃N)" by auto
qed

text‹If the axiom of choice holds for some cardinal,
then we can drop the compact sets of that cardial are compact of the same cardinal
as subspaces of every superspace.›

lemma Kcompact_subspace_imp_Kcompact:
  assumes "A{is compact of cardinal}Q{in}(T{restricted to}B)" "A⊆B" "({the axiom of} Q {choice holds})"
  shows "A{is compact of cardinal}Q{in}T"
proof -
  from assms(1) have a1:"Card(Q)" unfolding IsCompactOfCard_def RestrictedTo_def by auto
  from assms(1) have a2:"A⊆⋃T" unfolding IsCompactOfCard_def RestrictedTo_def by auto
  {
    fix M assume "M∈Pow(T)" "A⊆⋃M"
    let ?M="M{restricted to}B"
    from ‹M∈Pow(T)› have "?M∈Pow(T{restricted to}B)" unfolding RestrictedTo_def by auto
    from ‹A⊆⋃M› have "A⊆⋃?M" unfolding RestrictedTo_def using assms(2) by auto
    with assms ‹?M∈Pow(T{restricted to}B)› obtain N where N:"N∈Pow(?M)" "A⊆⋃N" "N ≺ Q" unfolding IsCompactOfCard_def by blast
    from N(3) have "N≲Q" using lesspoll_imp_lepoll by auto moreover 
    {
      fix BB assume "BB∈N"
      with ‹N∈Pow(?M)› have "BB∈?M" unfolding FinPow_def by auto
      then obtain S where "S∈M" and "BB=B∩S" unfolding RestrictedTo_def by auto
      then have "S∈{S∈M. B∩S=BB}" by auto
      then obtain "{S∈M. B∩S=BB}≠0" by auto
    }
    then have "∀BB∈N. ((λW∈N. {S∈M. B∩S=W})`BB)≠0" by auto moreover
    have " (N ≲ Q ∧ (∀t∈N. (λW∈N. {S∈M. B∩S=W}) ` t ≠ 0) ⟶ (∃f. f ∈ Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t) ∧ (∀t∈N. f ` t ∈ (λW∈N. {S∈M. B∩S=W}) ` t)))" 
      using assms(3) unfolding AxiomCardinalChoiceGen_def by blast
    ultimately
    obtain f where AA:"f∈Pi(N,λt. (λW∈N. {S∈M. B∩S=W}) ` t)" "∀t∈N. f`t∈(λW∈N. {S∈M. B∩S=W}) ` t" by blast
    from AA(2) have ss:"∀t∈N. f`t∈{S∈M. B∩S=t}" using beta_if by auto
    then have "{f`t. t∈N}⊆M" by auto
    {
      fix t assume "t∈N"
      with ss have "f`t∈{S∈M. B∩S∈N}" by auto
    }
    with AA(1) have FF:"f:N→{S∈M. B∩S∈N}" unfolding Pi_def Sigma_def using beta_if by auto moreover
    {
      fix aa bb assume AAA:"aa∈N" "bb∈N" "f`aa=f`bb"
      from AAA(1) ss have "B∩ (f`aa) =aa" by auto
      with AAA(3) have "B∩(f`bb)=aa" by auto
      with ss AAA(2) have "aa=bb" by auto
    }
    ultimately have "f∈inj(N,{S∈M. B∩S∈N})" unfolding inj_def by auto
    then have "f∈bij(N,range(f))" using inj_bij_range by auto
    then have "f∈bij(N,f``N)" using range_image_domain FF by auto
    then have "f∈bij(N,{f`t. t∈N})" using func_imagedef FF by auto
    then have "N≈{f`t. t∈N}" unfolding eqpoll_def by auto
    with ‹N≺Q› have "{f`t. t∈N}≺Q" using eqpoll_sym eq_lesspoll_trans by blast moreover
    with ss have "{f`t. t∈N}∈Pow(M)" unfolding FinPow_def by auto moreover
    {
      fix aa assume "aa∈A"
      with ‹A⊆⋃N› obtain b where "b∈N" and "aa∈b" by auto
      with ss have "B∩(f`b)=b" by auto
      with ‹aa∈b› have "aa∈B∩(f`b)" by auto
      then have "aa∈ f`b" by auto
      with ‹b∈N› have "aa∈⋃{f`t. t∈N}" by auto
    }
    then have "A⊆⋃{f`t. t∈N}" by auto ultimately
    have "∃R∈Pow(M). A⊆⋃R ∧ R≺Q" by auto
  }
  then show ?thesis using a1 a2 unfolding IsCompactOfCard_def by auto
qed

text‹Every set, with the cofinite topology is compact.›

lemma cofinite_compact:
  shows "X {is compact in}(CoFinite X)" unfolding IsCompact_def
proof
  show "X⊆⋃(CoFinite X)" using union_cocardinal unfolding Cofinite_def by auto
next
  {
    fix M assume "M∈Pow(CoFinite X)" "X⊆⋃M"
    {
      assume "M=0∨M={0}"
      then have "M∈FinPow(M)" unfolding FinPow_def by auto
      with ‹X⊆⋃M› have "∃N∈FinPow(M). X⊆⋃N" by auto
    }
    moreover
    {
      assume "M≠0""M≠{0}"
      then obtain U where "U∈M""U≠0" by auto
      with ‹M∈Pow(CoFinite X)› have "U∈CoFinite X" by auto
      with ‹U≠0› have "U⊆X" "(X-U)≺nat" unfolding Cofinite_def CoCardinal_def by auto
      then have "Finite(X-U)" using lesspoll_nat_is_Finite by auto
      then have "(X-U){is in the spectrum of}(λT. (⋃T){is compact in}T)" using compact_spectrum
        by auto
      then have "((⋃(CoFinite (X-U)))≈X-U) ⟶ ((⋃(CoFinite (X-U))){is compact in}(CoFinite (X-U)))" unfolding Spec_def
        using InfCard_nat CoCar_is_topology unfolding Cofinite_def by auto
      then have com:"(X-U){is compact in}(CoFinite (X-U))" using union_cocardinal unfolding Cofinite_def by auto
      have "(X-U)∩X=X-U" by auto
      then have "(CoFinite X){restricted to}(X-U)=(CoFinite (X-U))" using subspace_cocardinal unfolding Cofinite_def by auto
      with com have "(X-U){is compact in}(CoFinite X)" using compact_subspace_imp_compact[of "X-U""CoFinite X""X-U"] by auto
      moreover have "X-U⊆⋃M" using ‹X⊆⋃M› by auto
      moreover note ‹M∈Pow(CoFinite X)›
      ultimately have "∃N∈FinPow(M). X-U⊆⋃N" unfolding IsCompact_def by auto
      then obtain N where "N⊆M" "Finite(N)" "X-U⊆⋃N" unfolding FinPow_def by auto
      with ‹U∈M› have "N ∪{U}⊆M" "Finite(N ∪{U})" "X⊆⋃(N ∪{U})" by auto
      then have "∃N∈FinPow(M). X⊆⋃N" unfolding FinPow_def by blast
    }
    ultimately
    have "∃N∈FinPow(M). X⊆⋃N" by auto
  }
  then show "∀M∈Pow(CoFinite X). X ⊆ ⋃M ⟶ (∃N∈FinPow(M). X ⊆ ⋃N)" by auto
qed

text‹A corollary is then that the cofinite topology is locally compact; since every subspace
of a cofinite space is cofinite.›

corollary cofinite_locally_compact:
  shows "(CoFinite X){is locally-compact}"
proof-
  have cof:"topology0(CoFinite X)" and cof1:"(CoFinite X){is a topology}" 
    using CoCar_is_topology InfCard_nat Cofinite_def unfolding topology0_def by auto
  {
    fix x B assume "x∈⋃(CoFinite X)" "B∈(CoFinite X)" "x∈B"
    then have "x∈Interior(B,CoFinite X)" using topology0.Top_2_L3[OF cof] by auto moreover
    from ‹B∈(CoFinite X)› have "B⊆X" unfolding Cofinite_def CoCardinal_def by auto
    then have "B∩X=B" by auto
    then have "(CoFinite X){restricted to}B=CoFinite B" using subspace_cocardinal unfolding Cofinite_def by auto
    then have "B{is compact in}((CoFinite X){restricted to}B)" using cofinite_compact
      union_cocardinal unfolding Cofinite_def by auto
    then have "B{is compact in}(CoFinite X)" using compact_subspace_imp_compact by auto
    ultimately have "∃c∈Pow(B). x∈Interior(c,CoFinite X)∧ c{is compact in}(CoFinite X)" by auto
  }
  then have "(∀x∈⋃(CoFinite X). ∀b∈(CoFinite X). x∈b ⟶ (∃c∈Pow(b). x∈Interior(c,CoFinite X) ∧ c{is compact in}(CoFinite X)))"
    by auto
  then show ?thesis unfolding IsLocallyComp_def IsLocally_def[OF cof1] by auto
qed

text‹In every locally compact space, by definition, every point has a compact neighbourhood.›

theorem (in topology0) locally_compact_exist_compact_neig:
  assumes "T{is locally-compact}"
  shows "∀x∈⋃T. ∃A∈Pow(⋃T). A{is compact in}T ∧ x∈int(A)"
proof-
  {
    fix x assume "x∈⋃T" moreover
    then have "⋃T≠0" by auto
    have "⋃T∈T" using union_open topSpaceAssum by auto
    ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ c{is compact in}T" using assms 
      IsLocally_def topSpaceAssum unfolding IsLocallyComp_def by auto
    then have "∃c∈Pow(⋃T). c{is compact in}T ∧ x∈int(c)" by auto
  }
  then show ?thesis by auto
qed

text‹In Hausdorff spaces, the previous result is an equivalence.›

theorem (in topology0) exist_compact_neig_T2_imp_locally_compact:
  assumes "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A) ∧ A{is compact in}T" "T{is T⇩2}"
  shows "T{is locally-compact}"
proof-
  {
    fix x assume "x∈⋃T"
    with assms(1) obtain A where "A∈Pow(⋃T)" "x∈int(A)" and Acom:"A{is compact in}T" by blast
    then have Acl:"A{is closed in}T" using in_t2_compact_is_cl assms(2) by auto
    then have sub:"A⊆⋃T" unfolding IsClosed_def by auto
    {
      fix U assume "U∈T" "x∈U"
      let ?V="int(A∩U)"
      from ‹x∈U› ‹x∈int(A)› have "x∈U∩(int (A))" by auto
      moreover from ‹U∈T› have "U∩(int(A))∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def
        by auto moreover
      have "U∩(int(A))⊆A∩U" using Top_2_L1 by auto
      ultimately have "x∈?V" using Top_2_L5 by blast
      have "?V⊆A" using Top_2_L1 by auto
      then have "cl(?V)⊆A" using Acl Top_3_L13 by auto
      then have "A∩cl(?V)=cl(?V)" by auto moreover
      have clcl:"cl(?V){is closed in}T" using cl_is_closed ‹?V⊆A› ‹A⊆⋃T› by auto
      ultimately have comp:"cl(?V){is compact in}T" using Acom compact_closed[of "A""nat""T""cl(?V)"] Compact_is_card_nat
        by auto
      {
        then have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
          by auto moreover
        have "⋃(T{restricted to}cl(?V))=cl(?V)" unfolding RestrictedTo_def using clcl unfolding IsClosed_def by auto moreover
        ultimately have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
      }
      then have "(⋃(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto moreover
      have "(T{restricted to}cl(?V)){is T⇩2}" using assms(2) T2_here clcl unfolding IsClosed_def by auto
      ultimately have "(T{restricted to}cl(?V)){is T⇩4}" using topology0.T2_compact_is_normal unfolding topology0_def
        using Top_1_L4 unfolding isT4_def using T2_is_T1 by auto
      then have clvreg:"(T{restricted to}cl(?V)){is regular}" using topology0.T4_is_T3 unfolding topology0_def isT3_def using Top_1_L4
        by auto 
      have "?V⊆cl(?V)" using cl_contains_set ‹?V⊆A› ‹A⊆⋃T› by auto
      then have "?V∈(T{restricted to}cl(?V))" unfolding RestrictedTo_def using Top_2_L2 by auto
      with ‹x∈?V› obtain W where Wop:"W∈(T{restricted to}cl(?V))" and clcont:"Closure(W,(T{restricted to}cl(?V)))⊆?V" and cinW:"x∈W"
      using topology0.regular_imp_exist_clos_neig unfolding topology0_def using Top_1_L4 clvreg
        by blast
      from clcont Wop have "W⊆?V" using topology0.cl_contains_set unfolding topology0_def using Top_1_L4 by auto
      with Wop have "W∈(T{restricted to}cl(?V)){restricted to}?V" unfolding RestrictedTo_def by auto
      moreover from ‹?V⊆A› ‹A⊆⋃T› have "?V⊆⋃T" by auto
      then have "?V⊆cl(?V)""cl(?V)⊆⋃T" using ‹?V⊆cl(?V)› Top_3_L11(1) by auto
      then have "(T{restricted to}cl(?V)){restricted to}?V=(T{restricted to}?V)" using subspace_of_subspace by auto
      ultimately have "W∈(T{restricted to}?V)" by auto
      then obtain UU where "UU∈T" "W=UU∩?V" unfolding RestrictedTo_def by auto
      then have "W∈T" using Top_2_L2 topSpaceAssum unfolding IsATopology_def by auto moreover
      have "W⊆Closure(W,(T{restricted to}cl(?V)))" using topology0.cl_contains_set unfolding topology0_def
        using Top_1_L4 Wop by auto
      ultimately have A1:"x∈int(Closure(W,(T{restricted to}cl(?V))))" using Top_2_L6 cinW by auto
      from clcont have A2:"Closure(W,(T{restricted to}cl(?V)))⊆U" using Top_2_L1 by auto
      have clwcl:"Closure(W,(T{restricted to}cl(?V))) {is closed in}(T{restricted to}cl(?V))"
        using topology0.cl_is_closed Top_1_L4 Wop unfolding topology0_def by auto
      from comp have "cl(?V){is compact in}(T{restricted to}cl(?V))" using compact_imp_compact_subspace[of "cl(?V)""nat""T"] Compact_is_card_nat
          by auto
      with clwcl have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V)))))){is compact in}(T{restricted to}cl(?V))"
        using compact_closed Compact_is_card_nat by auto moreover
      from clcont have cont:"(Closure(W,(T{restricted to}cl(?V))))⊆cl(?V)" using cl_contains_set ‹?V⊆A›‹A⊆⋃T›
        by blast
      then have "((cl(?V)∩(Closure(W,(T{restricted to}cl(?V))))))=Closure(W,(T{restricted to}cl(?V)))" by auto
      ultimately have "Closure(W,(T{restricted to}cl(?V))){is compact in}(T{restricted to}cl(?V))" by auto
      then have "Closure(W,(T{restricted to}cl(?V))){is compact in}T" using compact_subspace_imp_compact[of "Closure(W,T{restricted to}cl(?V))"]
        cont by auto
      with A1 A2 have "∃c∈Pow(U). x∈int(c)∧c{is compact in}T" by auto
    }
    then have "∀U∈T. x∈U ⟶ (∃c∈Pow(U). x∈int(c)∧c{is compact in}T)" by auto
  }
  then show ?thesis unfolding IsLocally_def[OF topSpaceAssum] IsLocallyComp_def by auto
qed

subsection‹Compactification by one point›

text‹Given a topological space, we can always add one point to the space and get a new compact topology; as we
will check in this section.›

definition 
  OPCompactification ("{one-point compactification of}_" 90)
  where "{one-point compactification of}T≡T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}"

text‹Firstly, we check that what we defined is indeed a topology.›

theorem (in topology0) op_comp_is_top:
  shows "({one-point compactification of}T){is a topology}" unfolding IsATopology_def
proof(safe)
  fix M assume "M⊆{one-point compactification of}T"
  then have disj:"M⊆T∪{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}" unfolding OPCompactification_def by auto
  let ?MT="{A∈M. A∈T}"
  have "?MT⊆T" by auto
  then have c1:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto
  let ?MK="{A∈M. A∉T}"
  have "⋃M=⋃?MK ∪ ⋃?MT" by auto
  from disj have "?MK⊆{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto
  moreover have N:"⋃T∉(⋃T)" using mem_not_refl by auto
  {
    fix B assume "B∈M" "B∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}"
    then obtain K where "K∈Pow(⋃T)" "B={⋃T}∪((⋃T)-K)" by auto
    with N have "⋃T∈B" by auto
    with N have "B∉T" by auto
    with ‹B∈M› have "B∈?MK" by auto
  }
  then have "{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}⊆?MK" by auto
  ultimately have MK_def:"?MK={A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto
  let ?KK="{K∈Pow(⋃T). {⋃T}∪((⋃T)-K)∈?MK}"
  {
    assume "?MK=0"
    then have "⋃M=⋃?MT" by auto
    then have "⋃M∈T" using c1 by auto
    then have "⋃M∈{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  moreover
  {
    assume "?MK≠0"
    then obtain A where "A∈?MK" by auto
    then obtain K1 where "A={⋃T}∪((⋃T)-K1)" "K1∈Pow(⋃T)" "K1{is closed in}T" "K1{is compact in}T" using MK_def by auto
    with ‹A∈?MK› have "⋂?KK⊆K1" by auto
    from ‹A∈?MK› ‹A={⋃T}∪((⋃T)-K1)› ‹K1∈Pow(⋃T)› have "?KK≠0" by blast
    {
      fix K assume "K∈?KK"
      then have "{⋃T}∪((⋃T)-K)∈?MK" "K⊆⋃T" by auto
      then obtain KK where A:"{⋃T}∪((⋃T)-K)={⋃T}∪((⋃T)-KK)" "KK⊆⋃T" "KK{is compact in}T" "KK{is closed in}T" using MK_def by auto
      note A(1) moreover
      have "(⋃T)-K⊆{⋃T}∪((⋃T)-K)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-KK)" by auto
      ultimately have "(⋃T)-K⊆{⋃T}∪((⋃T)-KK)" "(⋃T)-KK⊆{⋃T}∪((⋃T)-K)" by auto moreover
      from N have "⋃T∉(⋃T)-K" "⋃T∉(⋃T)-KK" by auto ultimately
      have "(⋃T)-K⊆((⋃T)-KK)" "(⋃T)-KK⊆((⋃T)-K)" by auto
      then have "(⋃T)-K=(⋃T)-KK" by auto moreover
      from ‹K⊆⋃T› have "K=(⋃T)-((⋃T)-K)" by auto ultimately
      have "K=(⋃T)-((⋃T)-KK)" by auto
      with ‹KK⊆⋃T› have "K=KK" by auto
      with A(4) have "K{is closed in}T" by auto
    }
    then have "∀K∈?KK. K{is closed in}T" by auto
    with ‹?KK≠0› have "(⋂?KK){is closed in}T" using Top_3_L4 by auto
    with ‹K1{is compact in}T› have "(K1∩(⋂?KK)){is compact in}T" using Compact_is_card_nat
      compact_closed[of "K1""nat""T""⋂?KK"] by auto moreover
    from ‹⋂?KK⊆K1› have "K1∩(⋂?KK)=(⋂?KK)" by auto ultimately
    have "(⋂?KK){is compact in}T" by auto
    with ‹(⋂?KK){is closed in}T› ‹⋂?KK⊆K1› ‹K1∈Pow(⋃T)› have "({⋃T}∪((⋃T)-(⋂?KK)))∈({one-point compactification of}T)"
      unfolding OPCompactification_def by blast
    have t:"⋃?MK=⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}"
      using MK_def by auto
    {
      fix x assume "x∈⋃?MK"
      with t have "x∈⋃{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" by auto 
      then have "∃AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}. x∈AA"
        using Union_iff by auto
      then obtain AA where AAp:"AA∈{A∈M. A∈{{⋃T}∪((⋃T)-K). K∈{B∈Pow(⋃T). B{is compact in}T ∧ B{is closed in}T}}}" "x∈AA" by auto
      then obtain K2 where "AA={⋃T}∪((⋃T)-K2)" "K2∈Pow(⋃T)""K2{is compact in}T" "K2{is closed in}T" by auto
      with ‹x∈AA› have "x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)" by auto
      from ‹K2∈Pow(⋃T)› ‹AA={⋃T}∪((⋃T)-K2)› AAp(1) MK_def have "K2∈?KK" by auto
      then have "⋂?KK⊆K2" by auto
      with ‹x=⋃T ∨ (x∈(⋃T) ∧ x∉K2)› have "x=⋃T∨(x∈⋃T ∧ x∉⋂?KK)" by auto
     then have "x∈{⋃T}∪((⋃T)-(⋂?KK))" by auto
    }
    then have "⋃?MK⊆{⋃T}∪((⋃T)-(⋂?KK))" by auto
    moreover
    {
      fix x assume "x∈{⋃T}∪((⋃T)-(⋂?KK))"
      then have "x=⋃T∨(x∈(⋃T)∧ x∉⋂?KK)" by auto
      with ‹?KK≠0› obtain K2 where "K2∈?KK" "x=⋃T∨(x∈⋃T∧ x∉K2)" by auto
      then have "{⋃T}∪((⋃T)-K2)∈?MK" by auto
      with ‹x=⋃T∨(x∈⋃T∧ x∉K2)› have "x∈⋃?MK" by auto
    }
    then have "{⋃T}∪((⋃T)-(⋂?KK))⊆⋃?MK" by (safe,auto)
    ultimately have "⋃?MK={⋃T}∪((⋃T)-(⋂?KK))" by blast
    from ‹⋃?MT∈T› have "⋃T-(⋃T-⋃?MT)=⋃?MT" by auto
    with ‹⋃?MT∈T› have "(⋃T-⋃?MT){is closed in}T" unfolding IsClosed_def by auto
    have "((⋃T)-(⋂?KK))∪(⋃T-(⋃T-⋃?MT))=(⋃T)-((⋂?KK)∩(⋃T-⋃?MT))" by auto
    then have "({⋃T}∪((⋃T)-(⋂?KK)))∪(⋃T-(⋃T-⋃?MT))={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto
    with ‹⋃?MK={⋃T}∪((⋃T)-(⋂?KK))›‹⋃T-(⋃T-⋃?MT)=⋃?MT› have "⋃?MK∪⋃?MT={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))"
    by auto
    with ‹⋃M=⋃?MK ∪⋃?MT› have unM:"⋃M={⋃T}∪((⋃T)-((⋂?KK)∩(⋃T-⋃?MT)))" by auto
    have "((⋂?KK)∩(⋃T-⋃?MT)) {is closed in}T" using ‹(⋂?KK){is closed in}T›‹(⋃T-(⋃?MT)){is closed in}T›
      Top_3_L5 by auto
    moreover  
    note ‹(⋃T-(⋃?MT)){is closed in}T› ‹(⋂?KK){is compact in}T›
    then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact of cardinal}nat{in}T" using compact_closed[of "⋂?KK""nat""T""(⋃T-⋃?MT)"] Compact_is_card_nat
      by auto
    then have "((⋂?KK)∩(⋃T-⋃?MT)){is compact in}T" using Compact_is_card_nat by auto
    ultimately have "{⋃T}∪(⋃T-((⋂?KK)∩(⋃T-⋃?MT)))∈{one-point compactification of}T"
      unfolding OPCompactification_def IsClosed_def by auto
    with unM have "⋃M∈{one-point compactification of}T" by auto
  }
  ultimately show "⋃M∈{one-point compactification of}T" by auto
next
  fix U V assume "U∈{one-point compactification of}T" and "V∈{one-point compactification of}T"
  then have A:"U∈T∨(∃KU∈Pow(⋃T). U={⋃T}∪(⋃T-KU)∧KU{is closed in}T∧KU{is compact in}T)"
    "V∈T∨(∃KV∈Pow(⋃T). V={⋃T}∪(⋃T-KV)∧KV{is closed in}T∧KV{is compact in}T)" unfolding OPCompactification_def
    by auto
 have N:"⋃T∉(⋃T)" using mem_not_refl by auto
  {
    assume "U∈T""V∈T"
    then have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
    then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def
    by auto
  }
  moreover
  {
    assume "U∈T""V∉T"
    then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)"
    using A(2) by auto
    with N ‹U∈T› have "⋃T∉U" by auto
    then have "⋃T∉U∩V" by auto
    then have "U∩V=U∩(⋃T-KV)" using V(3) by auto
    moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto
    with ‹U∈T› have "U∩(⋃T-KV)∈T" using topSpaceAssum unfolding IsATopology_def by auto
    with ‹U∩V=U∩(⋃T-KV)› have "U∩V∈T" by auto
    then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
    }
  moreover
  {
    assume "U∉T""V∈T"
    then obtain KV where V:"KV{is closed in}T""KV{is compact in}T""U={⋃T}∪(⋃T-KV)"
    using A(1) by auto
    with N ‹V∈T› have "⋃T∉V" by auto
    then have "⋃T∉U∩V" by auto
    then have "U∩V=(⋃T-KV)∩V" using V(3) by auto
    moreover have "⋃T-KV∈T" using V(1) unfolding IsClosed_def by auto
    with ‹V∈T› have "(⋃T-KV)∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
    with ‹U∩V=(⋃T-KV)∩V› have "U∩V∈T" by auto
    then have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  moreover
  {
    assume "U∉T""V∉T"
    then obtain KV KU where V:"KV{is closed in}T""KV{is compact in}T""V={⋃T}∪(⋃T-KV)"
     and U:"KU{is closed in}T""KU{is compact in}T""U={⋃T}∪(⋃T-KU)"
    using A by auto
    with V(3) U(3) have "⋃T∈U∩V" by auto
    then have "U∩V={⋃T}∪((⋃T-KV)∩(⋃T-KU))" using V(3) U(3) by auto
    moreover have "⋃T-KV∈T""⋃T-KU∈T" using V(1) U(1) unfolding IsClosed_def by auto
    then have "(⋃T-KV)∩(⋃T-KU)∈T" using topSpaceAssum unfolding IsATopology_def by auto
    then have "(⋃T-KV)∩(⋃T-KU)=⋃T-(⋃T-((⋃T-KV)∩(⋃T-KU)))" by auto moreover
    with ‹(⋃T-KV)∩(⋃T-KU)∈T› have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is closed in}T" unfolding IsClosed_def
      by auto moreover
    from V(1) U(1) have "(⋃T-(⋃T-KV)∩(⋃T-KU))=KV∪KU" unfolding IsClosed_def by auto
    with V(2) U(2) have "(⋃T-(⋃T-KV)∩(⋃T-KU)){is compact in}T" using union_compact[of "KV""nat""T""KU"] Compact_is_card_nat
      InfCard_nat by auto ultimately
    have "U∩V∈{one-point compactification of}T" unfolding OPCompactification_def by auto
  }
  ultimately show "U∩V∈{one-point compactification of}T" by auto
qed

text‹The original topology is an open subspace of the new topology.›

theorem (in topology0) open_subspace:
  shows "⋃T∈{one-point compactification of}T" and "({one-point compactification of}T){restricted to}⋃T=T"
proof-
  show "⋃T∈{one-point compactification of}T"
  unfolding OPCompactification_def using topSpaceAssum unfolding IsATopology_def by auto
  have "T⊆({one-point compactification of}T){restricted to}⋃T" unfolding OPCompactification_def RestrictedTo_def by auto
  moreover
  {
    fix A assume "A∈({one-point compactification of}T){restricted to}⋃T"
    then obtain R where "R∈({one-point compactification of}T)" "A=⋃T∩R" unfolding RestrictedTo_def by auto
    then obtain K where K:"R∈T ∨ (R={⋃T}∪(⋃T-K) ∧ K{is closed in}T)" unfolding OPCompactification_def by auto
    with ‹A=⋃T∩R› have "(A=R∧R∈T)∨(A=⋃T-K ∧ K{is closed in}T)" using mem_not_refl unfolding IsClosed_def by auto
    with K have "A∈T" unfolding IsClosed_def by auto
  }
  ultimately
  show "({one-point compactification of}T){restricted to}⋃T=T" by auto
qed

text‹We added only one new point to the space.›

lemma (in topology0) op_compact_total:
  shows "⋃({one-point compactification of}T)={⋃T}∪(⋃T)"
proof-
  have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
  moreover note Top_3_L2 ultimately have TT:"0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto
  have "⋃({one-point compactification of}T)=(⋃T)∪(⋃{{⋃T}∪(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" unfolding OPCompactification_def
    by blast
  also have "…=(⋃T)∪{⋃T}∪(⋃{(⋃T-K). K∈{B∈Pow(⋃T). B{is compact in}T∧B{is closed in}T}})" using TT by auto
  ultimately show "⋃({one-point compactification of}T)={⋃T}∪(⋃T)" by auto
qed

text‹The one point compactification, gives indeed a compact topological space.›

theorem (in topology0) compact_op:
  shows "({⋃T}∪(⋃T)){is compact in}({one-point compactification of}T)" unfolding IsCompact_def
proof(safe)
  have "0{is compact in}T" unfolding IsCompact_def FinPow_def by auto
  moreover note Top_3_L2 ultimately have "0∈{A∈Pow(⋃T). A{is compact in}T ∧A{is closed in}T}" by auto
  then have "{⋃T}∪(⋃T)∈{one-point compactification of}T" unfolding OPCompactification_def by auto
  then show "⋃T ∈ ⋃{one-point compactification of}T" by auto
next
  fix x B assume "x∈B""B∈T"
  then show "x∈⋃({one-point compactification of}T)" using open_subspace by auto
next
  fix M assume A:"M⊆({one-point compactification of}T)" "{⋃T} ∪ ⋃T ⊆ ⋃M"
  then obtain R where "R∈M""⋃T∈R" by auto
  have "⋃T∉⋃T" using mem_not_refl by auto
  with ‹R∈M› ‹⋃T∈R› A(1) obtain K where K:"R={⋃T}∪(⋃T-K)" "K{is compact in}T""K{is closed in}T"
    unfolding OPCompactification_def by auto
  from K(1,2) have B:"{⋃T} ∪ (⋃T) = R ∪ K" unfolding IsCompact_def by auto
  with A(2) have "K⊆⋃M" by auto
  from K(2) have "K{is compact in}(({one-point compactification of}T){restricted to}⋃T)" using open_subspace(2)
    by auto
  then have "K{is compact in}({one-point compactification of}T)" using compact_subspace_imp_compact
    ‹K{is closed in}T› unfolding IsClosed_def by auto
  with ‹K⊆⋃M› A(1) have "(∃N∈FinPow(M). K ⊆ ⋃N)" unfolding IsCompact_def by auto
  then obtain N where "N∈FinPow(M)" "K⊆⋃N" by auto
  with ‹R∈M› have "(N ∪{R})∈FinPow(M)""R∪K⊆⋃(N∪{R})" unfolding FinPow_def by auto
  with B show "∃N∈FinPow(M). {⋃T} ∪ (⋃T)⊆⋃N" by auto
qed

text‹The one point compactification is Hausdorff iff the original space is also
Hausdorff and locally compact.›

lemma (in topology0) op_compact_T2_1:
  assumes "({one-point compactification of}T){is T⇩2}"
  shows "T{is T⇩2}"
  using T2_here[OF assms, of "⋃T"] open_subspace by auto

lemma (in topology0) op_compact_T2_2:
  assumes "({one-point compactification of}T){is T⇩2}"
  shows "T{is locally-compact}"
proof-
  {
    fix x assume "x∈⋃T"
    then have "x∈{⋃T}∪(⋃T)" by auto
    moreover have "⋃T∈{⋃T}∪(⋃T)" by auto moreover
    from ‹x∈⋃T› have "x≠⋃T" using mem_not_refl by auto
    ultimately have "∃U∈{one-point compactification of}T. ∃V∈{one-point compactification of}T. x ∈ U ∧ (⋃T) ∈ V ∧ U ∩ V = 0"
      using assms op_compact_total unfolding isT2_def by auto
    then obtain U V where UV:"U∈{one-point compactification of}T""V∈{one-point compactification of}T"
      "x∈U""⋃T∈V""U∩V=0" by auto
    from ‹V∈{one-point compactification of}T› ‹⋃T∈V› mem_not_refl obtain K where K:"V={⋃T}∪(⋃T-K)""K{is closed in}T""K{is compact in}T"
      unfolding OPCompactification_def by auto
    from ‹U∈{one-point compactification of}T› have "U⊆{⋃T}∪(⋃T)" unfolding OPCompactification_def 
      using op_compact_total by auto
    with ‹U∩V=0› K have "U⊆K""K⊆⋃T" unfolding IsClosed_def by auto
    then have "(⋃T)∩U=U" by auto moreover
    from UV(1) have "((⋃T)∩U)∈({one-point compactification of}T){restricted to}⋃T" 
      unfolding RestrictedTo_def by auto
    ultimately have "U∈T" using open_subspace(2) by auto
    with ‹x∈U›‹U⊆K› have "x∈int(K)" using Top_2_L6 by auto
    with ‹K⊆⋃T› ‹K{is compact in}T› have "∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto
  }
  then have "∀x∈⋃T. ∃A∈Pow(⋃T). x∈int(A)∧ A{is compact in}T" by auto
  then show ?thesis using op_compact_T2_1[OF assms] exist_compact_neig_T2_imp_locally_compact
    by auto
qed

lemma (in topology0) op_compact_T2_3:
  assumes "T{is locally-compact}" "T{is T⇩2}"
  shows "({one-point compactification of}T){is T⇩2}"
proof-
  {
    fix x y assume "x≠y""x∈⋃({one-point compactification of}T)""y∈⋃({one-point compactification of}T)"
    then have S:"x∈{⋃T}∪(⋃T)""y∈{⋃T}∪(⋃T)" using op_compact_total by auto
    {
      assume "x∈⋃T""y∈⋃T"
      with ‹x≠y› have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(2) unfolding isT2_def by auto
      then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0"
        unfolding OPCompactification_def by auto
    }
    moreover
    {
      assume "x∉⋃T∨y∉⋃T"
      with S have "x=⋃T∨y=⋃T" by auto
      with ‹x≠y› have "(x=⋃T∧y≠⋃T)∨(y=⋃T∧x≠⋃T)" by auto
      with S have "(x=⋃T∧y∈⋃T)∨(y=⋃T∧x∈⋃T)" by auto
      then obtain Ky Kx where "(x=⋃T∧ Ky{is compact in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧x∈int(Kx))"
        using assms(1) locally_compact_exist_compact_neig by blast
      then have "(x=⋃T∧ Ky{is compact in}T∧ Ky{is closed in}T∧y∈int(Ky))∨(y=⋃T∧ Kx{is compact in}T∧ Kx{is closed in}T∧x∈int(Kx))"
        using in_t2_compact_is_cl assms(2) by auto
      then have "(x∈{⋃T}∪(⋃T-Ky)∧y∈int(Ky)∧ Ky{is compact in}T∧ Ky{is closed in}T)∨(y∈{⋃T}∪(⋃T-Kx)∧x∈int(Kx)∧ Kx{is compact in}T∧ Kx{is closed in}T)"
        by auto moreover
      {
        fix K
        assume A:"K{is closed in}T""K{is compact in}T"
        then have "K⊆⋃T" unfolding IsClosed_def by auto
        moreover have "⋃T∉⋃T" using mem_not_refl by auto
        ultimately have "({⋃T}∪(⋃T-K))∩K=0" by auto
        then have "({⋃T}∪(⋃T-K))∩int(K)=0" using Top_2_L1 by auto moreover
        from A have "{⋃T}∪(⋃T-K)∈({one-point compactification of}T)" unfolding OPCompactification_def
          IsClosed_def by auto moreover
        have "int(K)∈({one-point compactification of}T)" using Top_2_L2 unfolding OPCompactification_def
          by auto ultimately
        have "int(K)∈({one-point compactification of}T)∧{⋃T}∪(⋃T-K)∈({one-point compactification of}T)∧({⋃T}∪(⋃T-K))∩int(K)=0"
          by auto
      }
      ultimately have "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0) ∨
        ({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)" by auto
      moreover
      {
        assume "({⋃T} ∪ (⋃T - Ky)∈({one-point compactification of}T)∧int(Ky)∈({one-point compactification of}T)∧x ∈ {⋃T} ∪ (⋃T - Ky) ∧ y ∈ int(Ky) ∧ ({⋃T}∪(⋃T-Ky))∩int(Ky)=0)"
        then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "int(Ky)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0" "{⋃T}∪(⋃T-Ky)"]
          by auto          
      } moreover
      {
        assume "({⋃T} ∪ (⋃T - Kx)∈({one-point compactification of}T)∧int(Kx)∈({one-point compactification of}T)∧y ∈ {⋃T} ∪ (⋃T - Kx) ∧ x ∈ int(Kx) ∧ ({⋃T}∪(⋃T-Kx))∩int(Kx)=0)"
        then have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" using exI[OF exI[of _ "{⋃T}∪(⋃T-Kx)"],of "λU V. U∈({one-point compactification of}T)∧V∈({one-point compactification of}T) ∧ x∈U∧y∈V∧U∩V=0""int(Kx)" ]
          by blast
      }
      ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto
    }
    ultimately have "∃U∈({one-point compactification of}T). ∃V∈({one-point compactification of}T). x∈U∧y∈V∧U∩V=0" by auto
  }
  then show ?thesis unfolding isT2_def by auto
qed

text‹In conclusion, every locally compact Hausdorff topological space is regular; since this property is hereditary.›

corollary (in topology0) locally_compact_T2_imp_regular:
  assumes "T{is locally-compact}" "T{is T⇩2}"
  shows "T{is regular}"
proof-
  from assms have "( {one-point compactification of}T) {is T⇩2}" using op_compact_T2_3 by auto
  then have "({one-point compactification of}T) {is T⇩4}" unfolding isT4_def using T2_is_T1 topology0.T2_compact_is_normal
    op_comp_is_top unfolding topology0_def using op_compact_total compact_op by auto
  then have "({one-point compactification of}T) {is T⇩3}" using topology0.T4_is_T3 op_comp_is_top unfolding topology0_def
    by auto
  then have "({one-point compactification of}T) {is regular}" using isT3_def by auto moreover
  have "⋃T⊆⋃({one-point compactification of}T)" using op_compact_total by auto
  ultimately have "(({one-point compactification of}T){restricted to}⋃T) {is regular}" using regular_here by auto
  then show "T{is regular}" using open_subspace(2) by auto
qed

text‹This last corollary has an explanation: In Hausdorff spaces, compact sets are closed
and regular spaces are exactly the "locally closed spaces"(those which have a neighbourhood basis of closed sets).
So the neighbourhood basis of compact sets also works as the neighbourhood basis of closed sets we needed to find.›

definition
  IsLocallyClosed ("_{is locally-closed}")
  where "T{is locally-closed} ≡ T{is locally}(λB TT. B{is closed in}TT)"

lemma (in topology0) regular_locally_closed:
  shows "T{is regular} ⟷ (T{is locally-closed})"
proof
  assume "T{is regular}"
  then have a:"∀x∈⋃T. ∀U∈T. (x∈U) ⟶ (∃V∈T. x ∈ V ∧ cl(V) ⊆ U)"  using regular_imp_exist_clos_neig by auto
  {
    fix x b assume "x∈⋃T""b∈T""x∈b"
    with a obtain V where "V∈T""x∈V""cl(V)⊆b" by blast
    note ‹cl(V)⊆b› moreover
    from ‹V∈T› have "V⊆⋃T" by auto
    then have "V⊆cl(V)" using cl_contains_set by auto
    with ‹x∈V›‹V∈T› have "x∈int(cl(V))" using Top_2_L6 by auto moreover
    from ‹V⊆⋃T› have "cl(V){is closed in}T" using cl_is_closed by auto
    ultimately have "x∈int(cl(V))""cl(V)⊆b""cl(V){is closed in}T" by auto
    then have "∃K∈Pow(b). x∈int(K)∧K{is closed in}T" by auto
  }
  then show "T{is locally-closed}" unfolding IsLocally_def[OF topSpaceAssum] IsLocallyClosed_def
    by auto
next
  assume "T{is locally-closed}"
  then have a:"∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃K∈Pow(b). x∈int(K)∧K{is closed in}T)" unfolding IsLocally_def[OF topSpaceAssum]
    IsLocallyClosed_def by auto
  {
    fix x b assume "x∈⋃T""b∈T""x∈b"
    with a obtain K where K:"K⊆b""x∈int(K)""K{is closed in}T" by blast
    have "int(K)⊆K" using Top_2_L1 by auto
    with K(3) have "cl(int(K))⊆K" using Top_3_L13 by auto
    with K(1) have "cl(int(K))⊆b" by auto moreover
    have "int(K)∈T" using Top_2_L2 by auto moreover
    note ‹x∈int(K)› ultimately have "∃V∈T. x∈V∧ cl(V)⊆b" by auto
  }
  then have "∀x∈⋃T. ∀b∈T. x∈b ⟶ (∃V∈T. x∈V∧ cl(V)⊆b)" by auto
  then show "T{is regular}" using exist_clos_neig_imp_regular by auto
qed

subsection‹Hereditary properties and local properties›

text‹In this section, we prove a relation between a property and its local property
for hereditary properties. Then we apply it to locally-Hausdorff or locally-$T_2$.
We also prove the relation between locally-$T_2$ and
another property that appeared when considering anti-properties, the
anti-hyperconnectness.›

text‹If a property is hereditary in open sets, then local properties are equivalent
to find just one open neighbourhood with that property instead of a whole local basis.›

lemma (in topology0) her_P_is_loc_P:
  assumes "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧P(B,TT) ⟶ P(B∩A,TT)"
  shows "(T{is locally}P) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧P(A,T))"
proof
  assume A:"T{is locally}P"
  {
    fix x assume x:"x∈⋃T"
    with A have "∀b∈T. x∈b ⟶ (∃c∈Pow(b). x∈int(c)∧P(c,T))" unfolding IsLocally_def[OF topSpaceAssum]
      by auto moreover
    note x moreover
    have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto
    ultimately have "∃c∈Pow(⋃T). x∈int(c)∧ P(c,T)" by auto
    then obtain c where c:"c⊆⋃T""x∈int(c)""P(c,T)" by auto
    have P:"int(c)∈T" using Top_2_L2 by auto moreover
    from c(1,3) topSpaceAssum assms have "∀A∈T. P(c∩A,T)" by auto
    ultimately have "P(c∩int(c),T)" by auto moreover
    from Top_2_L1[of "c"] have "int(c)⊆c" by auto
    then have "c∩int(c)=int(c)" by auto
    ultimately have "P(int(c),T)" by auto
    with P c(2) have "∃V∈T. x∈V∧P(V,T)" by auto
  }
  then show "∀x∈⋃T. ∃V∈T. x∈V∧P(V,T)" by auto
  next
  assume A:"∀x∈⋃T. ∃A∈T. x ∈ A ∧ P(A, T)"
  {
    fix x assume x:"x∈⋃T"
    {
      fix b assume b:"x∈b""b∈T"
      from x A obtain A where A_def:"A∈T""x∈A""P(A,T)" by auto
      from A_def(1,3) assms topSpaceAssum have "∀G∈T. P(A∩G,T)" by auto
      with b(2) have "P(A∩b,T)" by auto
      moreover from b(1) A_def(2) have "x∈A∩b" by auto moreover
      have "A∩b∈T" using b(2) A_def(1) topSpaceAssum IsATopology_def by auto
      then have "int(A∩b)=A∩b" using Top_2_L3 by auto
      ultimately have "x∈int(A∩b)∧P(A∩b,T)" by auto
      then have "∃c∈Pow(b). x∈int(c)∧P(c,T)" by auto
    }
    then have "∀b∈T. x∈b⟶(∃c∈Pow(b). x∈int(c)∧P(c,T))" by auto
  }
  then show "T{is locally}P" unfolding IsLocally_def[OF topSpaceAssum] by auto
qed


definition
  IsLocallyT2 ("_{is locally-T⇩2}" 70)
  where "T{is locally-T⇩2}≡T{is locally}(λB. λT. (T{restricted to}B){is T⇩2})"

text‹Since $T_2$ is an hereditary property, we can apply the previous lemma.›

corollary (in topology0) loc_T2:
  shows "(T{is locally-T⇩2}) ⟷ (∀x∈⋃T. ∃A∈T. x∈A∧(T{restricted to}A){is T⇩2})"
proof-
  {
    fix TT B A assume TT:"TT{is a topology}" "(TT{restricted to}B){is T⇩2}" "A∈TT""B∈Pow(⋃TT)"
    then have s:"B∩A⊆B""B⊆⋃TT" by auto
    then have "(TT{restricted to}(B∩A))=(TT{restricted to}B){restricted to}(B∩A)" using subspace_of_subspace
      by auto moreover
    have "⋃(TT{restricted to}B)=B" unfolding RestrictedTo_def using s(2) by auto
    then have "B∩A⊆⋃(TT{restricted to}B)" using s(1) by auto moreover
    note TT(2) ultimately have "(TT{restricted to}(B∩A)){is T⇩2}" using T2_here
      by auto
  }
  then have "∀TT. ∀B∈Pow(⋃TT). ∀A∈TT. TT{is a topology}∧(TT{restricted to}B){is T⇩2} ⟶ (TT{restricted to}(B∩A)){is T⇩2}"
    by auto
  with her_P_is_loc_P[where P="λA. λTT. (TT{restricted to}A){is T⇩2}"] show ?thesis unfolding IsLocallyT2_def by auto
qed


text‹First, we prove that a locally-$T_2$ space is anti-hyperconnected.›

text‹Before starting, let's prove that an open subspace of an hyperconnected
space is hyperconnected.›

lemma(in topology0) open_subspace_hyperconn:
  assumes "T{is hyperconnected}" "U∈T"
  shows "(T{restricted to}U){is hyperconnected}"
proof-
  {
    fix A B assume "A∈(T{restricted to}U)""B∈(T{restricted to}U)""A∩B=0"
    then obtain AU BU where "A=U∩AU""B=U∩BU" "AU∈T""BU∈T" unfolding RestrictedTo_def by auto
    then have "A∈T""B∈T" using topSpaceAssum assms(2) unfolding IsATopology_def by auto
    with ‹A∩B=0› have "A=0∨B=0" using assms(1) unfolding IsHConnected_def by auto
  }
  then show ?thesis unfolding IsHConnected_def by auto
qed

lemma(in topology0) locally_T2_is_antiHConn:
  assumes "T{is locally-T⇩2}"
  shows "T{is anti-}IsHConnected"
proof-
  {
    fix A assume A:"A∈Pow(⋃T)""(T{restricted to}A){is hyperconnected}"
    {
      fix x assume "x∈A"
      with A(1) have "x∈⋃T" by auto moreover
      have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately
      have "∃c∈Pow(⋃T). x ∈ int(c) ∧ (T {restricted to} c) {is T⇩2}" using assms
        unfolding IsLocallyT2_def IsLocally_def[OF topSpaceAssum] by auto
      then obtain c where c:"c∈Pow(⋃T)""x∈int(c)""(T {restricted to} c) {is T⇩2}" by auto
      have "⋃(T {restricted to} c)=(⋃T)∩c" unfolding RestrictedTo_def by auto
      with ‹c∈Pow(⋃T)›‹⋃T∈T› have tot:"⋃(T {restricted to} c)=c" by auto
      have "int(c)∈T" using Top_2_L2 by auto
      then have "A∩(int(c))∈(T{restricted to}A)" unfolding RestrictedTo_def by auto
      with A(2) have "((T{restricted to}A){restricted to}(A∩(int(c)))){is hyperconnected}"
        using topology0.open_subspace_hyperconn unfolding topology0_def using Top_1_L4
        by auto
      then have "(T{restricted to}(A∩(int(c)))){is hyperconnected}" using subspace_of_subspace[of "A∩(int(c))"
        "A""T"] A(1) by force moreover
      have "int(c)⊆c" using Top_2_L1 by auto
      then have sub:"A∩(int(c))⊆c" by auto
      then have "A∩(int(c))⊆⋃(T {restricted to} c)" using tot by auto
      then have "((T {restricted to} c){restricted to}(A∩(int(c)))) {is T⇩2}" using
        T2_here[OF c(3)] by auto
      with sub have "(T {restricted to}(A∩(int(c)))){is T⇩2}" using subspace_of_subspace[of "A∩(int(c))"
        "c""T"] ‹c∈Pow(⋃T)› by auto
      ultimately have "(T{restricted to}(A∩(int(c)))){is hyperconnected}""(T {restricted to}(A∩(int(c)))){is T⇩2}"
        by auto
      then have "(T{restricted to}(A∩(int(c)))){is hyperconnected}""(T {restricted to}(A∩(int(c)))){is anti-}IsHConnected"
        using topology0.T2_imp_anti_HConn unfolding topology0_def using Top_1_L4 by auto
      moreover
      have "⋃(T{restricted to}(A∩(int(c))))=(⋃T)∩A∩(int(c))" unfolding RestrictedTo_def by auto
      with A(1) Top_2_L2 have "⋃(T{restricted to}(A∩(int(c))))=A∩(int(c))" by auto
      then have "A∩(int(c))⊆⋃(T{restricted to}(A∩(int(c))))" by auto moreover
      have "A∩(int(c))⊆⋃T" using A(1) Top_2_L2 by auto
      then have "(T{restricted to}(A∩(int(c)))){restricted to}(A∩(int(c)))=(T{restricted to}(A∩(int(c))))"
        using subspace_of_subspace[of "A∩(int(c))""A∩(int(c))""T"] by auto
      ultimately have "(A∩(int(c))){is in the spectrum of}IsHConnected" unfolding antiProperty_def
        by auto
      then have "A∩(int(c))≲1" using HConn_spectrum by auto
      then have "(A∩(int(c))={x})" using lepoll_1_is_sing ‹x∈A›‹x∈int(c)› by auto
      then have "{x}∈(T{restricted to}A)" using ‹(A∩(int(c))∈(T{restricted to}A))› by auto 
    }
    then have pointOpen:"∀x∈A. {x}∈(T{restricted to}A)" by auto
    {
      fix x y assume "x≠y""x∈A""y∈A"
      with pointOpen have "{x}∈(T{restricted to}A)""{y}∈(T{restricted to}A)""{x}∩{y}=0"
        by auto
      with A(2) have "{x}=0∨{y}=0" unfolding IsHConnected_def by auto
      then have "False" by auto
    }
    then have uni:"∀x∈A. ∀y∈A. x=y" by auto
    {
      assume "A≠0"
      then obtain x where "x∈A" by auto
      with uni have "A={x}" by auto
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
    }
    moreover
    {
      assume "A=0"
      then have "A≈0" by auto
      then have "A≲1" using empty_lepollI eq_lepoll_trans by auto
    }
    ultimately have "A≲1" by auto
    then have "A{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
  }
  then show ?thesis unfolding antiProperty_def by auto
qed  

text‹Now we find a counter-example for: Every anti-hyperconnected space is locally-Hausdorff.›

text‹The example we are going to consider is the following. Put
in $X$ an anti-hyperconnected topology, where an infinite number of points don't
have finite sets as neighbourhoods. Then add a new point to the set, $p\notin X$.
Consider the open sets on $X\cup {p}$ as the anti-hyperconnected topology and
the open sets that contain $p$ are $p\cup A$ where $X\setminus A$ is finite.›

text‹This construction equals the one-point compactification iff
$X$ is anti-compact; i.e., the only compact sets are the finite ones.
In general this topology is contained in the one-point compactification topology,
making it compact too.›

text‹It is easy to check that any open set containing $p$ meets infinite other non-empty
open set. The question is if such a topology exists.›

theorem (in topology0) COF_comp_is_top:
  assumes "T{is T⇩1}""¬(⋃T≺nat)"
  shows "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T) {is a topology}"
proof-
  have N:"⋃T∉(⋃T)" using mem_not_refl by auto    
  {
    fix M assume M:"M⊆((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)"
    let ?MT="{A∈M. A∈T}"
    let ?MK="{A∈M. A∉T}"
    have MM:"(⋃?MT)∪(⋃?MK)=⋃M" by auto
    have MN:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto
    then have sub:"?MK⊆({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}"
      using M by auto
    then have "?MK⊆({one-point compactification of}(CoFinite (⋃T)))" by auto
    then have CO:"⋃?MK∈({one-point compactification of}(CoFinite (⋃T)))" using 
      topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]] unfolding Cofinite_def
      IsATopology_def by auto
    {
      assume AS:"⋃?MK={⋃T}"
      moreover have "∀R∈?MK. R⊆⋃?MK" by auto
      ultimately have "∀R∈?MK. R⊆{⋃T}" by auto
      then have "∀R∈?MK. R={⋃T}∨R=0" by force moreover
      with sub have "∀R∈?MK. R=0" by auto
      then have "⋃?MK=0" by auto
      with AS have "False" by auto
    }
    with CO have CO2:"⋃?MK∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
    {
      assume "⋃?MK∈(CoFinite (⋃T))"
      then have "⋃?MK∈T" using assms(1) T1_cocardinal_coarser by auto
      with MN have "{⋃?MT,⋃?MK}⊆(T)" by auto
      then have "(⋃?MT)∪(⋃?MK)∈T" using union_open[OF topSpaceAssum, of "{⋃?MT,⋃?MK}"] by auto
      then have "⋃M∈T" using MM by auto
    }
    moreover
    {
      assume "⋃?MK∉(CoFinite (⋃T))"
      with CO obtain B where "B{is compact in}(CoFinite (⋃T))""B{is closed in}(CoFinite (⋃T))"
        "⋃?MK={⋃CoFinite ⋃T}∪(⋃(CoFinite ⋃T)-B)" unfolding OPCompactification_def by auto
      then have MK:"⋃?MK={⋃T}∪(⋃T-B)""B{is closed in}(CoFinite (⋃T))"
        using union_cocardinal unfolding Cofinite_def by auto
      then have B:"B⊆⋃T" "B≺nat∨B=⋃T" using closed_sets_cocardinal unfolding Cofinite_def by auto
      {
        assume "B=⋃T"
        with MK have "⋃?MK={⋃T}" by auto
        then have "False" using CO2 by auto
      }
      with B have "B⊆⋃T" and natB:"B≺nat" by auto
      have "(⋃T-(⋃?MT))∩B⊆B" by auto
      then have "(⋃T-(⋃?MT))∩B≲B" using subset_imp_lepoll by auto
      then have "(⋃T-(⋃?MT))∩B≺nat" using natB lesspoll_trans1 by auto
      then have "((⋃T-(⋃?MT))∩B){is closed in}(CoFinite (⋃T))" using closed_sets_cocardinal
        B(1) unfolding Cofinite_def by auto
      then have "⋃T-((⋃T-(⋃?MT))∩B)∈(CoFinite (⋃T))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto
      also have "⋃T-((⋃T-(⋃?MT))∩B)=(⋃T-(⋃T-(⋃?MT)))∪(⋃T-B)" by auto
      also have "…=(⋃?MT)∪(⋃T-B)" by auto
      ultimately have P:"(⋃?MT)∪(⋃T-B)∈(CoFinite (⋃T))" by auto
      then have eq:"⋃T-(⋃T-((⋃?MT)∪(⋃T-B)))=(⋃?MT)∪(⋃T-B)" by auto
      from P eq have "(⋃T-((⋃?MT)∪(⋃T-B))){is closed in}(CoFinite (⋃T))" unfolding IsClosed_def
        using union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto moreover
      have "(⋃T-((⋃?MT)∪(⋃T-B)))∩⋃T=(⋃T-((⋃?MT)∪(⋃T-B)))" by auto
      then have "(CoFinite ⋃T){restricted to}(⋃T-((⋃?MT)∪(⋃T-B)))=CoFinite (⋃T-((⋃?MT)∪(⋃T-B)))" using subspace_cocardinal unfolding Cofinite_def by auto
      then have "(⋃T-((⋃?MT)∪(⋃T-B))){is compact in}((CoFinite ⋃T){restricted to}(⋃T-((⋃?MT)∪(⋃T-B))))" using cofinite_compact
        union_cocardinal unfolding Cofinite_def by auto
      then have "(⋃T-((⋃?MT)∪(⋃T-B))){is compact in}(CoFinite ⋃T)" using compact_subspace_imp_compact by auto ultimately
      have "{⋃T}∪(⋃T-(⋃T-((⋃?MT)∪(⋃T-B))))∈({one-point compactification of}(CoFinite (⋃T)))"
        unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto
      with eq have "{⋃T}∪((⋃?MT)∪(⋃T-B))∈({one-point compactification of}(CoFinite (⋃T)))" by auto
      moreover have AA:"{⋃T}∪((⋃?MT)∪(⋃T-B))=((⋃?MT)∪(⋃?MK))" using MK(1) by auto
      ultimately have AA2:"((⋃?MT)∪(⋃?MK))∈({one-point compactification of}(CoFinite (⋃T)))" by auto
      {
        assume AS:"(⋃?MT)∪(⋃?MK)={⋃T}"
        from MN have T:"⋃T∉⋃?MT" using N by auto
        {
          fix x assume G:"x∈⋃?MT"
          then have "x∈(⋃?MT)∪(⋃?MK)" by auto
          with AS have "x∈{⋃T}" by auto
          then have "x=⋃T" by auto
          with T have "False" using G by auto
        }
        then have "⋃?MT=0" by auto
        with AS have "(⋃?MK)={⋃T}" by auto
        then have "False" using CO2 by auto
      }
      with AA2 have "((⋃?MT)∪(⋃?MK))∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
      with MM have "⋃M∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
    }
    ultimately
    have "⋃M∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
  }
  then have "∀M∈Pow((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T). ⋃M∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T"
    by auto moreover
  {
    fix U V assume "U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T""V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" moreover
    {
      assume "U∈T""V∈T"
      then have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
      then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
    }
    moreover
    {
      assume UV:"U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})""V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})"
      then have O:"U∩V∈({one-point compactification of}(CoFinite (⋃T)))" using topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]] unfolding Cofinite_def
        IsATopology_def by auto
      then have "⋃T∩(U∩V)∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T"
        unfolding RestrictedTo_def by auto
      then have "⋃T∩(U∩V)∈CoFinite ⋃T" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]]
        union_cocardinal unfolding Cofinite_def by auto
      from UV have "U≠{⋃T}""V≠{⋃T}""⋃T∩U∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T""⋃T∩V∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T"
        unfolding RestrictedTo_def by auto
      then have R:"U≠{⋃T}""V≠{⋃T}""⋃T∩U∈CoFinite ⋃T""⋃T∩V∈CoFinite ⋃T" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]]
        union_cocardinal unfolding Cofinite_def by auto
      from UV have "U⊆⋃({one-point compactification of}(CoFinite (⋃T)))""V⊆⋃({one-point compactification of}(CoFinite (⋃T)))" by auto
      then have "U⊆{⋃T}∪⋃T""V⊆{⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat]]
        union_cocardinal unfolding Cofinite_def by auto
      then have E:"U=(⋃T∩U)∪({⋃T}∩U)""V=(⋃T∩V)∪({⋃T}∩V)""U∩V=(⋃T∩U∩V)∪({⋃T}∩U∩V)" by auto
      {
        assume Q:"U∩V={⋃T}"
        then have RR:"⋃T∩(U∩V)=0" using N by auto
        {
          assume "⋃T∩U=0"
          with E(1) have "U={⋃T}∩U" by auto
          also have "…⊆{⋃T}" by auto
          ultimately have "U⊆{⋃T}" by auto
          then have "U=0∨U={⋃T}" by auto
          with R(1) have "U=0" by auto
          then have "U∩V=0" by auto
          then have "False" using Q by auto
        }
        moreover
        {
          assume "⋃T∩V=0"
          with E(2) have "V={⋃T}∩V" by auto
          also have "…⊆{⋃T}" by auto
          ultimately have "V⊆{⋃T}" by auto
          then have "V=0∨V={⋃T}" by auto
          with R(2) have "V=0" by auto
          then have "U∩V=0" by auto
          then have "False" using Q by auto
        }
        moreover
        {
          assume "⋃T∩U≠0""⋃T∩V≠0"
          with R(3,4) have "(⋃T∩U)∩(⋃T∩V)≠0" using Cofinite_nat_HConn[OF assms(2)]
            unfolding IsHConnected_def by auto
          then have "⋃T∩(U∩V)≠0" by auto
          then have "False" using RR by auto
        }
        ultimately have "False" by auto
      }
      with O have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
    }
    moreover
    {
      assume UV:"U∈T""V∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}"
      from UV(2) obtain B where "V∈(CoFinite ⋃T)∨(V={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" unfolding OPCompactification_def
        using union_cocardinal unfolding Cofinite_def by auto
      with assms(1) have "V∈T∨(V={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using T1_cocardinal_coarser by auto
      then have "V∈T∨(U∩V=U∩(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using UV(1) N by auto
      then have "V∈T∨(U∩V=U∩(⋃T-B)∧(⋃T-B)∈(CoFinite (⋃T)))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto
      then have "V∈T∨(U∩V=U∩(⋃T-B)∧(⋃T-B)∈T)" using assms(1) T1_cocardinal_coarser by auto
      with UV(1) have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
      then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
    }
    moreover
    {
      assume UV:"U∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}""V∈T"
      from UV(1) obtain B where "U∈(CoFinite ⋃T)∨(U={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" unfolding OPCompactification_def
        using union_cocardinal unfolding Cofinite_def by auto
      with assms(1) have "U∈T∨(U={⋃T}∪(⋃T-B)∧B{is closed in}(CoFinite (⋃T)))" using T1_cocardinal_coarser by auto
      then have "U∈T∨(U∩V=(⋃T-B)∩V∧B{is closed in}(CoFinite (⋃T)))" using UV(2) N by auto
      then have "U∈T∨(U∩V=(⋃T-B)∩V∧(⋃T-B)∈(CoFinite (⋃T)))" unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def by auto
      then have "U∈T∨(U∩V=(⋃T-B)∩V∧(⋃T-B)∈T)" using assms(1) T1_cocardinal_coarser by auto
      with UV(2) have "U∩V∈T" using topSpaceAssum unfolding IsATopology_def by auto
      then have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
    }
    ultimately
    have "U∩V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" by auto
  }
  ultimately show ?thesis unfolding IsATopology_def by auto
qed

text‹The previous construction preserves anti-hyperconnectedness.›

theorem (in topology0) COF_comp_antiHConn:
  assumes "T{is anti-}IsHConnected" "¬(⋃T≺nat)"
  shows "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T) {is anti-}IsHConnected"
proof-
  have N:"⋃T∉(⋃T)" using mem_not_refl by auto
  from assms(1) have T1:"T{is T⇩1}" using anti_HConn_imp_T1 by auto
  have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"]
        union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto 
  then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover
  have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T"
    by auto
  ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"]
    tot1 unfolding Cofinite_def by auto moreover
  {
    assume "⋃T=0"
    with assms(2) have "¬(0≺nat)" by auto
    then have "False" unfolding lesspoll_def using empty_lepollI eqpoll_0_is_0
      eqpoll_sym by auto
  }
  then have "⋃T≠0" by auto
  with N have Not:"¬(⋃T⊆{⋃T})" by auto
  {
    assume "{⋃T}∪⋃T={⋃T}" moreover
    have "⋃T⊆{⋃T}∪⋃T" by auto ultimately
    have "⋃T⊆{⋃T}" by auto
    with Not have "False" by auto
  }
  then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
  then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto
  then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover
  have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto
  then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto
  with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto
  ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto
  {
    fix A assume AS:"A⊆⋃T" "(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A) {is hyperconnected}"
    from AS(1,2) have e0:"((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A=(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}⋃T){restricted to}A"
      using subspace_of_subspace[of "A""⋃T""((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)"] TOT by auto
    have e1:"(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}(⋃T))=((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T)∪(T{restricted to}⋃T)"
      unfolding RestrictedTo_def by auto
    {
      fix A assume "A∈T{restricted to}⋃T"
      then obtain B where "B∈T""A=B∩⋃T" unfolding RestrictedTo_def by auto
      then have "A=B" by auto
      with ‹B∈T› have "A∈T" by auto
    }
    then have "T{restricted to}⋃T⊆T" by auto moreover
      {
      fix A assume "A∈T"
      then have "⋃T∩A=A" by auto
      with ‹A∈T› have "A∈T{restricted to}⋃T" unfolding RestrictedTo_def by auto
    }
    ultimately have "T{restricted to}⋃T=T" by auto moreover
    {
      fix A assume "A∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T"
      then obtain B where "B∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}""⋃T∩B=A" unfolding RestrictedTo_def by auto
      then have "B∈({one-point compactification of}(CoFinite (⋃T)))""⋃T∩B=A" by auto
      then have "A∈({one-point compactification of}(CoFinite (⋃T))){restricted to}⋃T" unfolding RestrictedTo_def by auto
      then have "A∈(CoFinite (⋃T))" using topology0.open_subspace(2)[OF topology0_CoCardinal[OF InfCard_nat]]
        union_cocardinal unfolding Cofinite_def by auto
      with T1 have "A∈T" using T1_cocardinal_coarser by auto
    }
    then have "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}){restricted to}⋃T⊆T" by auto
    moreover note e1 ultimately
    have "((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T) {restricted to} (⋃T)) =T" by auto
    with e0 have "((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A=T{restricted to}A" by auto
    with assms(1) AS have "A{is in the spectrum of}IsHConnected" unfolding antiProperty_def by auto
  }
  then have reg:"∀A∈Pow(⋃T). ((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}A) {is hyperconnected}) ⟶(A{is in the spectrum of}IsHConnected)" by auto
  have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto
  then have P:"⋃T∈((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)" by auto
  {
    fix B assume sub:"B∈Pow(⋃T ∪{⋃T})" and hyp:"((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B) {is hyperconnected})"
    from P have  subop:"⋃T∩B∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" unfolding RestrictedTo_def by auto
    with hyp have hypSub:"((((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B){restricted to}(⋃T∩B)){is hyperconnected}" using topology0.open_subspace_hyperconn
      topology0.Top_1_L4 COF_comp_is_top[OF T1 assms(2)] unfolding topology0_def by auto
    from sub TOT have "B ⊆ ⋃(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T)" by auto
    then have "(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}(⋃T∩B))=(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B){restricted to}(⋃T∩B)"
      using subspace_of_subspace[of "⋃T∩B""B""((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)"] by auto
    with hypSub have "((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}} ∪ T) {restricted to} (⋃T ∩ B)){is hyperconnected}" by auto
    with reg have "(⋃T∩B){is in the spectrum of}IsHConnected" by auto
    then have le:"⋃T∩B≲1" using HConn_spectrum by auto
    {
      fix x assume x:"x∈⋃T∩B"
      with le have sing:"⋃T∩B={x}" using lepoll_1_is_sing by auto
      {
        fix y assume y:"y∈B"
        then have "y∈⋃T ∪{⋃T}" using sub by auto
        with y have "y∈⋃T∩B∨y=⋃T" by auto
        with sing have "y=x∨y=⋃T" by auto
      }
      then have "B⊆{x,⋃T}" by auto
      with x have disj:"B={x}∨B={x,⋃T}" by auto
      {
        assume "⋃T∈B"
        with disj have B:"B={x,⋃T}" by auto
        from sing subop have singOp:"{x}∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)"
          by auto
        have "{x}{is closed in}(CoFinite ⋃T)" using topology0.T1_iff_singleton_closed[OF topology0_CoCardinal[OF InfCard_nat]] cocardinal_is_T1[OF InfCard_nat]
          x union_cocardinal unfolding Cofinite_def by auto
        moreover 
        have "Finite({x})" by auto
        then have spec:"{x}{is in the spectrum of} (λT. (⋃T) {is compact in}T)" using compact_spectrum by auto
        have "((CoFinite ⋃T){restricted to}{x}){is a topology}""⋃((CoFinite ⋃T){restricted to}{x})={x}"
          using topology0.Top_1_L4[OF topology0_CoCardinal[OF InfCard_nat]] unfolding RestrictedTo_def Cofinite_def
          using x union_cocardinal by auto
        with spec have "{x}{is compact in}((CoFinite ⋃T){restricted to}{x})" unfolding Spec_def
          by auto
        then have "{x}{is compact in}(CoFinite ⋃T)" using compact_subspace_imp_compact
          by auto moreover note x
        ultimately have "{⋃T}∪(⋃T-{x})∈{one-point compactification of}(CoFinite (⋃T))" unfolding OPCompactification_def
          using union_cocardinal unfolding Cofinite_def by auto moreover
        {
          assume A:"{⋃T}∪(⋃T-{x})={⋃T}"
          {
            fix y assume P:"y∈⋃T-{x}"
            then have "y∈{⋃T}∪(⋃T-{x})" by auto
            then have "y=⋃T" using A by auto
            with N P have "False" by auto
          }
          then have "⋃T-{x}=0" by auto
          with x have "⋃T={x}" by auto
          then have "⋃T≈1" using singleton_eqpoll_1 by auto moreover
          have "1≺nat" using n_lesspoll_nat by auto
          ultimately have "⋃T≺nat" using eq_lesspoll_trans by auto
          then have "False" using assms(2) by auto
        }
        ultimately have "{⋃T}∪(⋃T-{x})∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
        then have  "{⋃T}∪(⋃T-{x})∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T))" by auto
        then have "B∩({⋃T}∪(⋃T-{x}))∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" unfolding RestrictedTo_def by auto
        moreover have "B∩({⋃T}∪(⋃T-{x}))={⋃T}" using B by auto
        ultimately have "{⋃T}∈(((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T){restricted to}B)" by auto
        with singOp hyp N x have "False" unfolding IsHConnected_def by auto
      }
      with disj have "B={x}" by auto
      then have "B≈1" using singleton_eqpoll_1 by auto
      then have "B≲1" using eqpoll_imp_lepoll by auto
    }
    then have "⋃T∩B≠0⟶B≲1" by blast
    moreover
    {
      assume "⋃T∩B=0"
      with sub have "B⊆{⋃T}" by auto
      then have "B≲{⋃T}" using subset_imp_lepoll by auto
      then have "B≲1" using singleton_eqpoll_1 lepoll_eq_trans by auto
    }
    ultimately have "B≲1" by auto
    then have "B{is in the spectrum of}IsHConnected" using HConn_spectrum by auto
  }
  then show ?thesis unfolding antiProperty_def using TOT by auto
qed

text‹The previous construction, applied to a densely ordered topology, gives the desired counterexample.
What happends is that every neighbourhood of ‹⋃T› is dense; because there are no finite open
sets, and hence meets every non-empty open set. In conclusion, ‹⋃T› cannot be separated from other points
by disjoint open sets.›

text‹Every open set that contains ‹⋃T› is dense, when considering the order
topology in a densely ordered set with more than two points.›

theorem neigh_infPoint_dense:
  fixes T X r
  defines T_def:"T ≡ (OrdTopology X r)"
  assumes "IsLinOrder(X,r)" "X{is dense with respect to}r"
    "∃x y. x≠y∧x∈X∧y∈X" "U∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" "⋃T∈U"
    "V∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T" "V≠0"
  shows "U∩V≠0"
proof
  have N:"⋃T∉(⋃T)" using mem_not_refl by auto
  have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"]
        union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto 
  then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover
  have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T"
    by auto
  ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"]
    tot1 unfolding Cofinite_def by auto moreover
  {
    assume "⋃T=0"
    then have "X=0" unfolding T_def using union_ordtopology[OF assms(2)] assms(4) by auto
    then have "False" using assms(4) by auto
  }
  then have "⋃T≠0" by auto
  with N have Not:"¬(⋃T⊆{⋃T})" by auto
  {
    assume "{⋃T}∪⋃T={⋃T}" moreover
    have "⋃T⊆{⋃T}∪⋃T" by auto ultimately
    have "⋃T⊆{⋃T}" by auto
    with Not have "False" by auto
  }
  then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
  then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto
  then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover
  have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto
  then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto
  with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto
  ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto
  assume A:"U∩V=0"
  with assms(6) have NN:"⋃T∉V" by auto
  with assms(7) have "V∈(CoFinite ⋃T)∪T" unfolding OPCompactification_def using union_cocardinal
    unfolding Cofinite_def by auto
  moreover have "T{is T⇩2}" unfolding T_def using order_top_T2[OF assms(2)] assms(4) by auto
  then have T1:"T{is T⇩1}" using T2_is_T1 by auto
  ultimately have VopT:"V∈T" using topology0.T1_cocardinal_coarser[OF topology0_ordtopology(1)[OF assms(2)]]
    unfolding T_def by auto
  from A assms(7) have "V⊆⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)-U" by auto
  then have "V⊆({⋃T}∪⋃T)-U" using TOT by auto
  then have "V⊆(⋃T)-U" using NN by auto
  from N have "U∉T" using assms(6) by auto
  then have "U∉(CoFinite ⋃T)∪T" using T1 topology0.T1_cocardinal_coarser[OF topology0_ordtopology(1)[OF assms(2)]]
    unfolding T_def using union_cocardinal union_ordtopology[OF assms(2)] assms(4) by auto
  with assms(5,6) obtain B where U:"U={⋃T}∪(⋃T-B)" "B{is closed in}(CoFinite ⋃T)" "B≠⋃T"
    unfolding OPCompactification_def using union_cocardinal unfolding Cofinite_def by auto
  then have "U={⋃T}∪(⋃T-B)" "B=⋃T ∨ B≺nat" "B≠⋃T" using closed_sets_cocardinal unfolding Cofinite_def
    by auto
  then have "U={⋃T}∪(⋃T-B)" "B≺nat" by auto
  with N have "⋃T-U=⋃T-(⋃T-B)" by auto
  then have "⋃T-U=B" using U(2) unfolding IsClosed_def using union_cocardinal unfolding Cofinite_def
    by auto
  with ‹B≺nat› have "Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto
  with ‹V⊆(⋃T)-U› have "Finite(V)" using subset_Finite by auto
  from assms(8) obtain v where "v∈V" by auto
  with VopT have "∃R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪{RightRayX(X, r, b) . b ∈ X}. R ⊆ V ∧ v ∈ R" using 
    point_open_base_neigh[OF Ordtopology_is_a_topology(2)[OF assms(2)]] unfolding T_def by auto
  then obtain R where R_def:"R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪{RightRayX(X, r, b) . b ∈ X}" "R⊆V" "v∈R" by blast
  moreover
  {
    assume "R∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X}"
    then obtain b c where lim:"b∈X""c∈X""R=IntervalX(X, r, b, c)" by auto
    with ‹v∈R› have " ¬ Finite(R)" using dense_order_inf_intervals[OF assms(2) _ _ _ assms(3)] 
      by auto
    with ‹R⊆V› ‹Finite(V)› have "False" using subset_Finite by auto
  } moreover
  {
    assume "R∈{LeftRayX(X, r, b) . b ∈ X}"
    then obtain b where lim:"b∈X""R=LeftRayX(X, r, b)" by auto
    with ‹v∈R› have " ¬ Finite(R)" using dense_order_inf_lrays[OF assms(2) _ _ assms(3)] by auto 
    with ‹R⊆V› ‹Finite(V)› have "False" using subset_Finite by auto
  } moreover
  {
    assume "R∈{RightRayX(X, r, b) . b ∈ X}"
    then obtain b where lim:"b∈X""R=RightRayX(X, r, b)" by auto
    with ‹v∈R› have " ¬ Finite(R)" using dense_order_inf_rrays[OF assms(2)_ _ assms(3)] by auto
    with ‹R⊆V› ‹Finite(V)› have "False" using subset_Finite by auto
  } ultimately
  show "False" by auto
qed

text‹A densely ordered set with more than one point gives an order topology.
Applying the previous construction to this topology we get a non locally-Hausdorff space.›
  
theorem OPComp_cofinite_dense_order_not_loc_T2:
  fixes T X r
  defines T_def:"T ≡ (OrdTopology X r)"
  assumes "IsLinOrder(X,r)" "X{is dense with respect to}r"
    "∃x y. x≠y∧x∈X∧y∈X"
  shows "¬((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩2})"
proof
  have N:"⋃T∉(⋃T)" using mem_not_refl by auto
  have tot1:"⋃({one-point compactification of}(CoFinite (⋃T)))={⋃T}∪⋃T" using topology0.op_compact_total[OF topology0_CoCardinal[OF InfCard_nat], of "⋃T"]
        union_cocardinal[of "nat""⋃T"] unfolding Cofinite_def by auto 
  then have "(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T={⋃T}∪⋃T" by auto moreover
  have "⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)=(⋃({one-point compactification of}(CoFinite (⋃T))))∪⋃T"
    by auto
  ultimately have tot2:"⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)={⋃T}∪⋃T" by auto
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))" using union_open[OF topology0.op_comp_is_top[OF topology0_CoCardinal[OF InfCard_nat]],of "{one-point compactification of}(CoFinite (⋃T))"]
    tot1 unfolding Cofinite_def by auto moreover
  {
    assume "⋃T=0"
    then have "X=0" unfolding T_def using union_ordtopology[OF assms(2)] assms(4) by auto
    then have "False" using assms(4) by auto
  }
  then have "⋃T≠0" by auto
  with N have Not:"¬(⋃T⊆{⋃T})" by auto
  {
    assume "{⋃T}∪⋃T={⋃T}" moreover
    have "⋃T⊆{⋃T}∪⋃T" by auto ultimately
    have "⋃T⊆{⋃T}" by auto
    with Not have "False" by auto
  }
  then have "{⋃T}∪⋃T≠{⋃T}" by auto ultimately
  have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}" by auto
  then have "{⋃T}∪⋃T∈({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T" by auto
  then have "{⋃T}∪⋃T⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" by auto moreover
  have "({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T⊆({one-point compactification of}(CoFinite (⋃T)))∪T" by auto
  then have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆⋃(({one-point compactification of}(CoFinite (⋃T)))∪T)" by auto
  with tot2 have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)⊆{⋃T}∪⋃T" by auto
  ultimately have TOT:"⋃((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}})∪T)={⋃T}∪⋃T" by auto
  have T1:"T{is T⇩1}" using order_top_T2[OF assms(2,4)] T2_is_T1 unfolding T_def by auto moreover
  from assms(4) obtain b c where B:"b∈X""c∈X""b≠c" by auto
  {
    assume "⟨b,c⟩∉r"
    with assms(2) have "⟨c,b⟩∈r" unfolding IsLinOrder_def IsTotal_def using ‹b∈X›‹c∈X› by auto
    with assms(3) B obtain z where "z∈X-{b,c}""⟨c,z⟩∈r""⟨z,b⟩∈r" unfolding IsDense_def by auto
    then have "IntervalX(X,r,c,b)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
    then have "¬(Finite(IntervalX(X,r,c,b)))" using dense_order_inf_intervals[OF assms(2) _ ‹c∈X›‹b∈X› assms(3)]
      by auto moreover
    have "IntervalX(X,r,c,b)⊆X" unfolding IntervalX_def by auto
    ultimately have "¬(Finite(X))" using subset_Finite by auto
    then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto
  }
  moreover
  {
    assume "⟨b,c⟩∈r"
    with assms(3) B obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" unfolding IsDense_def by auto
    then have "IntervalX(X,r,b,c)≠0" unfolding IntervalX_def using Order_ZF_2_L1 by auto
    then have "¬(Finite(IntervalX(X,r,b,c)))" using dense_order_inf_intervals[OF assms(2) _ ‹b∈X›‹c∈X› assms(3)]
      by auto moreover
    have "IntervalX(X,r,b,c)⊆X" unfolding IntervalX_def by auto
    ultimately have "¬(Finite(X))" using subset_Finite by auto
    then have "¬(X≺nat)" using lesspoll_nat_is_Finite by auto
  }
  ultimately have "¬(X≺nat)" by auto
  with T1 have top:"(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is a topology}" using topology0.COF_comp_is_top[OF topology0_ordtopology[OF assms(2)]] unfolding T_def
    using union_ordtopology[OF assms(2,4)] by auto
  assume "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩2}" moreover
  have "⋃T∈⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" using TOT by auto
  moreover have "⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)∈(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)"
    using top unfolding IsATopology_def by auto
  ultimately have "∃c∈Pow(⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)). ⋃T ∈ Interior(c, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T) ∧
            ((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} c) {is T⇩2}" unfolding IsLocallyT2_def IsLocally_def[OF top] by auto
  then obtain C where C:"C⊆⋃(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T)" "⋃T ∈ Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)" and T2:"((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C) {is T⇩2}"
    by auto
  have sub:"Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)⊆C" using topology0.Top_2_L1
    top unfolding topology0_def by auto
  have "(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}C){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))=((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))"
    using subspace_of_subspace[OF sub C(1)] by auto moreover
  have "(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))⊆C" unfolding RestrictedTo_def by auto
  with C(1) have "(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))=C" unfolding RestrictedTo_def by auto
  with sub have pp:"Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)∈Pow(⋃((({one-point compactification of}CoFinite ⋃T) - {{⋃T}} ∪ T) {restricted to} C))" by auto
  ultimately have T2_2:"(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))){is T⇩2}"
    using T2_here[OF T2 pp] by auto
  have top2:"(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))){is a topology}"
    using topology0.Top_1_L4 top unfolding topology0_def by auto
  from C(2) pp have p1:"⋃T∈⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))"
    unfolding RestrictedTo_def by auto
    from top topology0.Top_2_L2 have intOP:"(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding topology0_def by auto
  {
    fix x assume "x≠⋃T" "x∈⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))"
    with p1 have "∃U∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))). ∃V∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))).
      x∈U∧⋃T∈V∧U∩V=0" using T2_2 unfolding isT2_def by auto
    then obtain U V where UV:"U∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))"
      "V∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))"
      "U≠0""⋃T∈V""U∩V=0" by auto
    from UV(1) obtain UC where "U=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩UC""UC∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))"
      unfolding RestrictedTo_def by auto
    with top intOP have Uop:"U∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding IsATopology_def by auto
    from UV(2) obtain VC where "V=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩VC""VC∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))"
      unfolding RestrictedTo_def by auto
    with top intOP have "V∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" unfolding IsATopology_def by auto
    with UV(3-5) Uop neigh_infPoint_dense[OF assms(2-4),of "V""U"] union_ordtopology[OF assms(2,4)]
      have "False" unfolding T_def by auto
  }
  then have "⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))⊆{⋃T}"
    by auto
  with p1 have "⋃(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))={⋃T}"
    by auto
  with top2 have "{⋃T}∈(((({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T){restricted to}(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T)))"
    unfolding IsATopology_def by auto
  then obtain W where UT:"{⋃T}=(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩W""W∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T"
    unfolding RestrictedTo_def by auto
  from this(2) have "(Interior(C, (({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T))∩W∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" using intOP
    top unfolding IsATopology_def by auto
  with UT(1) have "{⋃T}∈(({one-point compactification of}(CoFinite ⋃T)) - {{⋃T}}) ∪ T" by auto
  then have "{⋃T}∈T" by auto
  with N show "False" by auto
qed

text‹This topology, from the previous result, gives a counter-example for
anti-hyperconnected implies locally-$T_2$.›
  
theorem antiHConn_not_imp_loc_T2:
  fixes T X r
  defines T_def:"T ≡ (OrdTopology X r)"
  assumes "IsLinOrder(X,r)" "X{is dense with respect to}r"
    "∃x y. x≠y∧x∈X∧y∈X"
  shows "¬((({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is locally-T⇩2})"
  and "(({one-point compactification of}(CoFinite (⋃T)))-{{⋃T}}∪T){is anti-}IsHConnected"
  using OPComp_cofinite_dense_order_not_loc_T2[OF assms(2-4)] dense_order_infinite[OF assms(2-4)] union_ordtopology[OF assms(2,4)]
  topology0.COF_comp_antiHConn[OF topology0_ordtopology[OF assms(2)] topology0.T2_imp_anti_HConn[OF topology0_ordtopology[OF assms(2)] order_top_T2[OF assms(2,4)]]]
  unfolding T_def by auto

text‹Let's prove that $T_2$ spaces are locally-$T_2$, but that there
are locally-$T_2$ spaces which aren't $T_2$. In conclusion $T_2\Rightarrow$ locally
-$T_2\Rightarrow$ anti-hyperconnected; all implications proper.›

theorem(in topology0) T2_imp_loc_T2:
  assumes "T{is T⇩2}"
  shows "T{is locally-T⇩2}"
proof-
  {
    fix x assume "x∈⋃T"
    {
      fix b assume b:"b∈T""x∈b"
      then have "(T{restricted to}b){is T⇩2}" using T2_here assms by auto moreover
      from b have "x∈int(b)" using Top_2_L3 by auto
      ultimately have "∃c∈Pow(b). x∈int(c)∧(T{restricted to}c){is T⇩2}" by auto
    }
    then have "∀b∈T. x∈b ⟶(∃c∈Pow(b). x∈int(c)∧(T{restricted to}c){is T⇩2})" by auto
  }
  then show ?thesis unfolding IsLocallyT2_def IsLocally_def[OF topSpaceAssum] by auto
qed

text‹If there is a closed singleton, then we can consider a topology that
makes this point doble.›

theorem(in topology0) doble_point_top:
  assumes "{m}{is closed in}T"
  shows "(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is a topology}"
proof-
  {
    fix M assume M:"M⊆T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}"
    let ?MT="{V∈M. V∈T}"
    let ?Mm="{V∈M. V∉T}"
    have unm:"⋃M=(⋃?MT)∪(⋃?Mm)" by auto
    have tt:"⋃?MT∈T" using topSpaceAssum unfolding IsATopology_def by auto
    {
      assume "?Mm=0"
      then have "⋃?Mm=0" by auto
      with unm have "⋃M=(⋃?MT)" by auto
      with tt have "⋃M∈T" by auto
      then have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
    }
    moreover
    {
      assume AS:"?Mm≠0"
      then obtain V where V:"V∈M""V∉T" by auto
      with M have "V∈{(U - {m}) ∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast
      then obtain U W where U:"V=(U-{m})∪{⋃T}∪W" "U∈T""m∈U" "W∈T" by auto
      let ?U="{⟨V,W⟩∈T×T. m∈V∧ (V-{m})∪{⋃T}∪W∈?Mm}"
      let ?fU="{fst(B). B∈?U}"
      let ?sU="{snd(B). B∈?U}"
      have "?fU⊆T""?sU⊆T" by auto
      then have P:"⋃?fU∈T""⋃?sU∈T" using topSpaceAssum unfolding IsATopology_def by auto moreover
      have "⟨U,W⟩∈?U" using U V by auto
      then have "m∈⋃?fU" by auto
      ultimately have s:"⟨⋃?fU,⋃?sU⟩∈{V∈T. m∈V}×T" by auto
      moreover have r:"∀S. ∀R. S∈{V∈T. m∈V}⟶ R∈T⟶(S-{m})∪{⋃T}∪R∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}"
        by auto
      ultimately have "(⋃?fU-{m})∪{⋃T}∪⋃?sU∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      {
        fix v assume "v∈⋃?Mm"
        then obtain V where v:"v∈V""V∈?Mm" by auto
        then have V:"V∈M""V∉T" by auto
        with M have "V∈{U - {m} ∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast
        then obtain U W where U:"V=(U-{m})∪{⋃T}∪W" "U∈T""m∈U" "W∈T" by auto
        with v(1) have "v∈(U-{m})∪{⋃T}∪W" by auto
        then have "v∈U-{m}∨v=⋃T∨v∈W" by auto
        then have "(v∈U∧v≠m)∨v=⋃T∨v∈W" by auto
        moreover from U V have "⟨U,W⟩∈?U" by auto
        ultimately have "v∈((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by auto
      }
      then have "⋃?Mm⊆((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by blast moreover
      {
        fix v assume v:"v∈((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)"
        {
          assume "v=⋃T"
          then have "v∈(U-{m})∪{⋃T}∪W" by auto
          with ‹⟨U,W⟩∈?U› have "v∈⋃?Mm" by auto
        }
        moreover
        {
          assume "v≠⋃T""v∉⋃?sU"
          with v have "v∈((⋃?fU)-{m})" by auto
          then have "(v∈⋃?fU∧v≠m)" by auto
          then obtain W where "(v∈W∧W∈?fU∧v≠m)" by auto
          then have "v∈(W-{m})∪{⋃T}" "W∈?fU" by auto
          then obtain B where "fst(B)=W" "B∈?U" "v∈(W-{m})∪{⋃T}" by blast
          then have "v∈⋃?Mm" by auto
        }
        ultimately have "v∈⋃?Mm" by auto
      }
      then have "((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)⊆⋃?Mm" by auto
      ultimately have "⋃?Mm=((⋃?fU)-{m})∪{⋃T}∪(⋃?sU)" by auto
      then have "⋃M=((⋃?fU)-{m})∪{⋃T}∪((⋃?sU)∪(⋃?MT))" using unm by auto
      moreover from P tt have "(⋃?sU)∪(⋃?MT)∈T" using topSpaceAssum 
        union_open[OF topSpaceAssum, of "{⋃?sU,⋃?MT}"] by auto
      with s have "⟨⋃?fU,(⋃?sU)∪(⋃?MT)⟩∈{V∈T. m∈V}×T" by auto
      then have "((⋃?fU)-{m})∪{⋃T}∪((⋃?sU)∪(⋃?MT))∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" using r
        by auto
      ultimately have "⋃M∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      then have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
    }
    ultimately
    have "⋃M∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
  }
  then have "∀M∈Pow(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ⋃M∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
  moreover
  {
    fix A B assume ass:"A∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}""B∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}"
    {
      assume A:"A∈T"
      {
        assume "B∈T"
        with A have "A∩B∈T" using topSpaceAssum unfolding IsATopology_def by auto
      }
      moreover
      {
        assume "B∉T"
        with ass(2) have "B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
        then obtain U W where U:"U∈T""m∈U""W∈T""B=(U-{m})∪{⋃T}∪W" by auto moreover
        from A mem_not_refl have "⋃T∉A" by auto
        ultimately have "A∩B=A∩((U-{m})∪W)" by auto
        then have eq:"A∩B=(A∩(U-{m}))∪(A∩W)" by auto
        have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto
        with U(1) have O:"U∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        have "U∩(⋃T-{m})=U-{m}" using U(1) by auto
        with O have "U-{m}∈T" by auto
        with A have "(A∩(U-{m}))∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        moreover
        from A U(3) have "A∩W∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        ultimately have "(A∩(U-{m}))∪(A∩W)∈T" using
          union_open[OF topSpaceAssum, of "{A∩(U-{m}),A∩W}"] by auto
        with eq have "A∩B∈T" by auto
      }
      ultimately have "A∩B∈T" by auto
    }
    moreover
    {
      assume "A∉T"
      with ass(1) have A:"A∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto      
        {
        assume B:"B∈T"
        from A obtain U W where U:"U∈T""m∈U""W∈T""A=(U-{m})∪{⋃T}∪W" by auto moreover
        from B mem_not_refl have "⋃T∉B" by auto
        ultimately have "A∩B=((U-{m})∪W)∩B" by auto
        then have eq:"A∩B=((U-{m})∩B)∪(W∩B)" by auto
        have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto
        with U(1) have O:"U∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        have "U∩(⋃T-{m})=U-{m}" using U(1) by auto
        with O have "U-{m}∈T" by auto
        with B have "((U-{m})∩B)∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        moreover
        from B U(3) have "W∩B∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        ultimately have "((U-{m})∩B)∪(W∩B)∈T" using
          union_open[OF topSpaceAssum, of "{((U-{m})∩B),(W∩B)}"] by auto
        with eq have "A∩B∈T" by auto
      }
      moreover
      {
        assume "B∉T"
        with ass(2) have "B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
        then obtain U W where U:"U∈T""m∈U""W∈T""B=(U-{m})∪{⋃T}∪W" by auto moreover
        from A obtain UA WA where UA:"UA∈T""m∈UA""WA∈T""A=(UA-{m})∪{⋃T}∪WA" by auto
        ultimately have "A∩B=(((UA-{m})∪WA)∩((U-{m})∪W))∪{⋃T}" by auto
        then have eq:"A∩B=((UA-{m})∩(U-{m}))∪(WA∩(U-{m}))∪((UA-{m})∩W)∪(WA∩W)∪{⋃T}" by auto
        have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto
        with U(1) UA(1) have O:"U∩(⋃T-{m})∈T""UA∩(⋃T-{m})∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        have "U∩(⋃T-{m})=U-{m}""UA∩(⋃T-{m})=UA-{m}" using U(1) UA(1) by auto
        with O have OO:"U-{m}∈T""UA-{m}∈T" by auto
        then have "((UA-{m})∩(U-{m}))=UA∩U-{m}" by auto
        moreover
        have "UA∩U∈T""m∈UA∩U" using U(1,2) UA(1,2) topSpaceAssum unfolding IsATopology_def
          by auto
        moreover
        from OO U(3) UA(3) have TT:"WA∩(U-{m})∈T""(UA-{m})∩W∈T""WA∩W∈T" using topSpaceAssum unfolding IsATopology_def
          by auto
        from TT(2,3) have "((UA-{m})∩W)∪(WA∩W)∈T" using union_open[OF topSpaceAssum,
          of "{(UA-{m})∩W,WA∩W}"] by auto
        with TT(1) have "(WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W))∈T" using union_open[OF topSpaceAssum,
          of "{WA∩(U-{m}),((UA-{m})∩W)∪(WA∩W)}"] by auto
        ultimately
        have "A∩B=(UA∩U-{m})∪{⋃T}∪((WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W)))"
          "(WA∩(U-{m}))∪(((UA-{m})∩W)∪(WA∩W))∈T" "UA∩U∈{V∈T. m∈V}" using eq by auto
        then have "∃W∈T. A∩B=(UA∩U-{m})∪{⋃T}∪W" "UA∩U∈{V∈T. m∈V}" by auto
        then have "A∩B∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      }
      ultimately
      have "A∩B∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
    }
    ultimately have "A∩B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
  }
  then have "∀A∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}. ∀B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}.
    A∩B∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast
  ultimately show ?thesis unfolding IsATopology_def by auto
qed

text‹The previous topology is defined over a set with one more point.›

lemma(in topology0) union_doublepoint_top:
  assumes "{m}{is closed in}T"
  shows "⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})=⋃T ∪{⋃T}"
proof
  {
    fix x assume "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    then obtain R where x:"x∈R""R∈T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by blast
    {
      assume "R∈T"
      with x(1) have "x∈⋃T" by auto
    }
    moreover
    {
      assume "R∉T"
      with x(2) have "R∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      then obtain U W where "R=(U-{m})∪{⋃T}∪W""W∈T""U∈T""m∈U" by auto
      with x(1) have "x=⋃T∨x∈⋃T" by auto
    }
    ultimately have "x∈⋃T ∪{⋃T}" by auto
  }
  then show "⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})⊆⋃T ∪{⋃T}" by auto
  {
    fix x assume "x∈⋃T ∪{⋃T}"
    then have dis:"x∈⋃T∨x=⋃T" by auto
    {
      assume "x∈⋃T"
      then have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
    }
    moreover
    {
      assume "x∉⋃T"
      with dis have "x=⋃T" by auto
      moreover from assms have "⋃T-{m}∈T""m∈⋃T" unfolding IsClosed_def by auto
      moreover have "0∈T" using empty_open topSpaceAssum by auto
      ultimately have "x∈(⋃T-{m})∪{⋃T}∪0" "(⋃T-{m})∪{⋃T}∪0∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}"
        using union_open[OF topSpaceAssum] by auto
      then have "x∈(⋃T-{m})∪{⋃T}∪0" "(⋃T-{m})∪{⋃T}∪0∈T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}"
        by auto
      then have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by blast
    }
    ultimately have "x∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
  }
  then show "⋃T ∪{⋃T}⊆⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
qed

text‹In this topology, the previous topological space is an open subspace.›

theorem(in topology0) open_subspace_double_point:
  assumes "{m}{is closed in}T"
  shows "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T" and "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
proof-
  have N:"⋃T∉⋃T" using mem_not_refl by auto
  {
    fix x assume "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T"
    then obtain U where U:"U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})""x=⋃T∩U"
      unfolding RestrictedTo_def by blast
    {
      assume "U∉T"
      with U(1) have  "U∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      then obtain V W where VW:"U=(V-{m})∪{⋃T}∪W""V∈T""m∈V""W∈T" by auto
      with N U(2) have x:"x=(V-{m})∪W" by auto
      have "⋃T-{m}∈T" using assms unfolding IsClosed_def by auto
      then have "V∩(⋃T-{m})∈T" using VW(2) topSpaceAssum unfolding IsATopology_def
        by auto moreover
      have "V-{m}=V∩(⋃T-{m})" using VW(2,3) by auto ultimately
      have "V-{m}∈T" by auto
      with VW(4) have "(V-{m})∪W∈T" using union_open[OF topSpaceAssum, of "{V-{m},W}"]
        by auto
      with x have "x∈T" by auto
    }
    moreover
    {
      assume A:"U∈T"
      with U(2) have "x=U" by auto
      with A have "x∈T" by auto
    }
    ultimately have "x∈T" by auto
  }
  then have "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T⊆T" by auto
  moreover
  {
    fix x assume x:"x∈T"
    then have "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto moreover
    from x have "⋃T∩x=x" by auto ultimately
    have "∃M∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ⋃T∩M=x" by blast
    then have "x∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T" unfolding RestrictedTo_def
      by auto
  }
  ultimately show "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T" by auto
  have P:"⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto
  then show "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
qed
  
text‹The previous topology construction applied to a $T_2$ non-discrite space
topology, gives a counter-example to: Every locally-$T_2$ space
is $T_2$.›

text‹If there is a singleton which is not open, but closed; then the construction on that point
is not $T_2$.›

theorem(in topology0) loc_T2_imp_T2_counter_1:
  assumes "{m}∉T" "{m}{is closed in}T"
  shows "¬((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is T⇩2})"
proof
  assume ass:"(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is T⇩2}"
  then have tot1:"⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})=⋃T ∪{⋃T}" using union_doublepoint_top
    assms(2) by auto
  have "m≠⋃T" using mem_not_refl assms(2) unfolding IsClosed_def by auto moreover
  from ass tot1 have "∀x y. x∈⋃T ∪{⋃T} ∧ y∈⋃T ∪{⋃T}∧x≠y ⟶ (∃𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}).
    ∃𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). x∈𝔘∧y∈𝔙∧𝔘∩𝔙=0)" unfolding isT2_def by auto
  moreover
  from assms(2) have "m∈⋃T ∪{⋃T}" unfolding IsClosed_def by auto moreover
  have "⋃T∈⋃T ∪{⋃T}" by auto ultimately
  have "∃𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ∃𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). m∈𝔘∧⋃T∈𝔙∧𝔘∩𝔙=0"
    by auto
  then obtain 𝔘 𝔙 where UV:"𝔘∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})"
    "𝔙∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})""m∈𝔘""⋃T∈𝔙""𝔘∩𝔙=0" using tot1 by blast
  then have "⋃T∉𝔘" by auto
  with UV(1) have P:"𝔘∈T" by auto
  {
    assume "𝔙∈T"
    then have "𝔙⊆⋃T" by auto
    with UV(4) have "⋃T∈⋃T" using tot1 by auto
    then have "False" using mem_not_refl by auto
  }
  with UV(2) have "𝔙∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
  then obtain U W where V:"𝔙=(U-{m})∪{⋃T}∪W" "U∈T""m∈U""W∈T" by auto
  from V(2,3) P have int:"U∩𝔘∈T""m∈U∩𝔘" using UV(3) topSpaceAssum 
    unfolding IsATopology_def by auto
  have "(U∩𝔘-{m})⊆𝔘" "(U∩𝔘-{m})⊆𝔙" using V(1) by auto
  then have "(U∩𝔘-{m})=0" using UV(5) by auto
  with int(2) have "U∩𝔘={m}" by auto
  with int(1) assms(1) show "False" by auto
qed

text‹This topology is locally-$T_2$.›

theorem(in topology0) loc_T2_imp_T2_counter_2:
  assumes "{m}∉T" "m∈⋃T" "T{is T⇩2}"
  shows "(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}) {is locally-T⇩2}"
proof-
  from assms(3) have "T{is T⇩1}" using T2_is_T1 by auto
  with assms(2) have mc:"{m}{is closed in}T" using T1_iff_singleton_closed by auto
  have N:"⋃T∉⋃T" using mem_not_refl by auto
  have res:"(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T=T"
    and P:"⋃T∈T" and Q:"⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" using open_subspace_double_point mc
    topSpaceAssum unfolding IsATopology_def by auto
  {
    fix A assume ass:"A∈⋃T ∪{⋃T}"
    {
      assume "A≠⋃T"
      with ass have "A∈⋃T" by auto
      with Q res assms(3) have "⋃T∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})∧ A∈⋃T ∧ (((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}⋃T){is T⇩2})" by auto
      then have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩2})"
        by blast
    }
    moreover
    {
      assume A:"A=⋃T"
      have "⋃T∈T""m∈⋃T""0∈T" using assms(2) empty_open[OF topSpaceAssum] unfolding IsClosed_def using P by auto
      then have "(⋃T-{m})∪{⋃T}∪0∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
      then have opp:"(⋃T-{m})∪{⋃T}∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
      {
        fix A1 A2 assume points:"A1∈(⋃T-{m})∪{⋃T}""A2∈(⋃T-{m})∪{⋃T}""A1≠A2"
        from points(1,2) have notm:"A1≠m""A2≠m" using assms(2) unfolding IsClosed_def 
          using mem_not_refl by auto
        {
          assume or:"A1∈⋃T""A2∈⋃T"
          with points(3) assms(3) obtain U V where UV:"U∈T""V∈T""A1∈U""A2∈V"
            "U∩V=0" unfolding isT2_def by blast
          from UV(1,2) have "U∩((⋃T-{m})∪{⋃T})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})"
            "V∩((⋃T-{m})∪{⋃T})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})"
            unfolding RestrictedTo_def by auto moreover
          then have "U∩(⋃T-{m})=U∩((⋃T-{m})∪{⋃T})" "V∩(⋃T-{m})=V∩((⋃T-{m})∪{⋃T})" using UV(1,2) mem_not_refl[of "⋃T"]
            by auto
          ultimately have opUV:"U∩(⋃T-{m})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})"
            "V∩(⋃T-{m})∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" by auto
          moreover have "U∩(⋃T-{m})∩(V∩(⋃T-{m}))=0" using UV(5) by auto moreover
          from UV(3) or(1) notm(1) have "A1∈U∩(⋃T-{m})" by auto moreover
          from UV(4) or(2) notm(2) have "A2∈V∩(⋃T-{m})" by auto ultimately
          have "∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ A1∈U∩(⋃T-{m})∧A2∈V∧(U∩(⋃T-{m}))∩V=0" using exI[where x="V∩(⋃T-{m})" and P="λW. W∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧A1∈(U∩(⋃T-{m}))∧A2∈W∧(U∩(⋃T-{m}))∩W=0"]
            using opUV(2) by auto
          then have "∃U. U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧(∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧
            A1∈U∧A2∈V∧U∩V=0)" using exI[where x="U∩(⋃T-{m})" and P="λW. W∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧(∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ A1∈W∧A2∈V∧W∩V=0)"]
            using opUV(1) by auto
          then have "∃U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V. V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧A1∈U∧A2∈V∧U∩V=0)" by blast
          then have "∃U∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). A1∈U∧A2∈V∧U∩V=0)" by blast
        }
        moreover
        {
          assume "A1∉⋃T"
          then have ig:"A1=⋃T" using points(1) by auto
          {
            assume "A2∉⋃T"
            then have "A2=⋃T" using points(2) by auto
            with points(3) ig have "False" by auto
          }
          then have igA2:"A2∈⋃T" by auto moreover
          have "m∈⋃T" using assms(2) unfolding IsClosed_def by auto
          moreover note notm(2) assms(3) ultimately obtain U V where UV:"U∈T""V∈T"
            "m∈U""A2∈V""U∩V=0" unfolding isT2_def by blast
          from UV(1,3) have "U∈{W∈T. m∈W}" by auto moreover
          have "0∈T" using empty_open topSpaceAssum by auto ultimately
          have "(U-{m})∪{⋃T}∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
          then have Uop:"(U-{m})∪{⋃T}∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
          from UV(2) have Vop:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
          from UV(1-3,5) have sub:"V⊆(⋃T-{m})∪{⋃T}" "((U-{m})∪{⋃T})⊆(⋃T-{m})∪{⋃T}" by auto
          from sub(1) have "V=((⋃T-{m})∪{⋃T})∩V" by auto
          then have VV:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def
            using Vop by blast moreover
          from sub(2) have "((U-{m})∪{⋃T})=((⋃T-{m})∪{⋃T})∩((U-{m})∪{⋃T})" by auto
          then have UU:"((U-{m})∪{⋃T})∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def
            using Uop by blast moreover
          from UV(2) have "((U-{m})∪{⋃T})∩V=(U-{m})∩V" using mem_not_refl by auto
          then  have "((U-{m})∪{⋃T})∩V=0" using UV(5) by auto
          with UV(4) VV ig igA2 have "∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈(U-{m})∪{⋃T}∧A2∈V∧((U-{m})∪{⋃T})∩V=0" by auto
          with UU ig have "∃U. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)" using exI[where x="((U-{m})∪{⋃T})" and P="λU. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)"] by auto
          then have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)" by blast
        }
        moreover
        {
          assume "A2∉⋃T"
          then have ig:"A2=⋃T" using points(2) by auto
          {
            assume "A1∉⋃T"
            then have "A1=⋃T" using points(1) by auto
            with points(3) ig have "False" by auto
          }
          then have igA2:"A1∈⋃T" by auto moreover
          have "m∈⋃T" using assms(2) unfolding IsClosed_def by auto
          moreover note notm(1) assms(3) ultimately obtain U V where UV:"U∈T""V∈T"
            "m∈U""A1∈V""U∩V=0" unfolding isT2_def by blast
          from UV(1,3) have "U∈{W∈T. m∈W}" by auto moreover
          have "0∈T" using empty_open topSpaceAssum by auto ultimately
          have "(U-{m})∪{⋃T}∈{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}" by auto
          then have Uop:"(U-{m})∪{⋃T}∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
          from UV(2) have Vop:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T})" by auto
          from UV(1-3,5) have sub:"V⊆(⋃T-{m})∪{⋃T}" "((U-{m})∪{⋃T})⊆(⋃T-{m})∪{⋃T}" by auto
          from sub(1) have "V=((⋃T-{m})∪{⋃T})∩V" by auto
          then have VV:"V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def
            using Vop by blast moreover
          from sub(2) have "((U-{m})∪{⋃T})=((⋃T-{m})∪{⋃T})∩((U-{m})∪{⋃T})" by auto
          then have UU:"((U-{m})∪{⋃T})∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})" unfolding RestrictedTo_def
            using Uop by blast moreover
          from UV(2) have "V∩((U-{m})∪{⋃T})=V∩(U-{m})" using mem_not_refl by auto
          then have "V∩((U-{m})∪{⋃T})=0" using UV(5) by auto
          with UU UV(4) ig igA2 have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈V∧A2∈U∧V∩U=0" by auto
          with VV igA2 have "∃U. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)" using exI[where x="V" and P="λU. U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})∧ (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)"] by auto
          then have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)" by blast
        }
        ultimately have "∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0)" by blast
      }
      then have "∀A1∈(⋃T-{m})∪{⋃T}. ∀A2∈(⋃T-{m})∪{⋃T}. A1≠A2 ⟶ (∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0))" by auto moreover
      have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}))∩((⋃T-{m})∪{⋃T})"
        unfolding RestrictedTo_def by auto
      then have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃T ∪{⋃T})∩((⋃T-{m})∪{⋃T})" using 
        union_doublepoint_top mc by auto
      then have "⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}))=(⋃T-{m})∪{⋃T}" by auto
      ultimately have "∀A1∈⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})). ∀A2∈⋃((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})). A1≠A2 ⟶ (∃U∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}). (∃V∈(T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T}).
            A1∈U∧A2∈V∧U∩V=0))" by auto
      then have "((T ∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}((⋃T-{m})∪{⋃T})){is T⇩2}" unfolding isT2_def
        by force
      with opp A have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩2})"
        by blast
    }
    ultimately
    have "∃Z∈(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). A∈Z∧(((T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}){restricted to}Z){is T⇩2})"
        by blast
  }
  then have "∀A∈⋃(T∪{(U-{m})∪{⋃T}∪W. ⟨U,W⟩∈{V∈T. m∈V}×T}). ∃Z∈T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}.
     A ∈ Z ∧ ((T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}) {restricted to} Z) {is T⇩2}"
     using union_doublepoint_top mc by auto
  with topology0.loc_T2 show "(T ∪ {U - {m} ∪ {⋃T} ∪ W . ⟨U,W⟩ ∈ {V ∈ T . m ∈ V} × T}){is locally-T⇩2}"
    unfolding topology0_def using doble_point_top mc by auto
qed

text‹There can be considered many more local properties, which; as
happens with locally-$T_2$; can distinguish between spaces other properties cannot.›

end