Theory Topology_ZF_5

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

    Copyright (C) 2012-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 ‹Topology 5›

theory Topology_ZF_5 imports Topology_ZF_examples Topology_ZF_properties func1 Topology_ZF_examples_1 Topology_ZF_4
begin

subsection‹Some results for separation axioms›

text‹First we will give a global characterization of $T_1$-spaces; which is interesting
because it involves the cardinal $\mathbb{N}$.›

lemma (in topology0)  T1_cocardinal_coarser:
  shows "(T {is T⇩1}) ⟷ (CoFinite (⋃T))⊆T"
proof
  {
    assume AS:"T {is T⇩1}"
    {
      fix x assume p:"x∈⋃T"
      {
        fix y assume "y∈(⋃T)-{x}"
        with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast
        then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto
        then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
      }
      then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
      then have "⋃T-{x}∈T" using open_neigh_open by auto
      with p have "{x} {is closed in}T" using IsClosed_def by auto
    }
    then have pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto
    {
      fix A
      assume AS2:"A∈FinPow(⋃T)"
      let ?p="{⟨x,{x}⟩. x∈A}"
      have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto
      then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality
        by auto
      then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto
      with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto
      then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def
      by (safe, blast+) 
      then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto
      moreover
      have "⋃{{x}. x∈A}=A" by auto
      ultimately have "A {is closed in} T" by simp
    }
    then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto
    {
      fix U
      assume AS2:"U ∈ CoCardinal(⋃T,nat)"
      then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto
      then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto
      then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum
        reg unfolding FinPow_def by auto
      then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto
      moreover
      then have "(⋃T-(⋃T-U))=U" by blast
      ultimately have "U∈T" by auto
    }
    then show "(CoFinite (⋃T))⊆T" using Cofinite_def by auto
  }
  {
    assume "(CoFinite (⋃T))⊆T"
    then have AS:"CoCardinal(⋃T,nat) ⊆ T" using Cofinite_def by auto
    {
      fix x y
      assume AS2:"x∈⋃T" "y∈⋃T""x≠y"
      have "Finite({y})" by auto
      then obtain n where "{y}≈n" "n∈nat" using Finite_def by auto
      then have "{y}≺nat" using n_lesspoll_nat eq_lesspoll_trans by auto
      then have "{y} {is closed in} CoCardinal(⋃T,nat)" using closed_sets_cocardinal
        AS2(2) by auto
      then have "(⋃T)-{y}∈CoCardinal(⋃T,nat)" using union_cocardinal IsClosed_def by auto
      with AS have "(⋃T)-{y}∈T" by auto
      moreover
      with AS2(1,3) have "x∈((⋃T)-{y}) ∧ y∉((⋃T)-{y})" by auto
      ultimately have "∃V∈T. x∈V∧y∉V" by(safe,auto)
    }
    then show "T {is T⇩1}" using isT1_def by auto
  }
qed

text‹In the previous proof, it is obvious that we don't need to check
if ever cofinite set is open. It is enough to check if every singleton is closed.›

corollary(in topology0) T1_iff_singleton_closed:
  shows "(T {is T⇩1}) ⟷ (∀x∈⋃T. {x}{is closed in}T)"
proof
  assume AS:"T {is T⇩1}"
  {
    fix x assume p:"x∈⋃T"
    {
      fix y assume "y∈(⋃T)-{x}"
      with AS p obtain U where "U∈T" "y∈U" "x∉U" using isT1_def by blast
      then have "U∈T" "y∈U" "U⊆(⋃T)-{x}" by auto
      then have "∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
    }
    then have "∀y∈(⋃T)-{x}. ∃U∈T. y∈U ∧ U⊆(⋃T)-{x}" by auto
    then have "⋃T-{x}∈T" using open_neigh_open by auto
    with p have "{x} {is closed in}T" using IsClosed_def by auto
  }
  then show pointCl:"∀x∈⋃T. {x} {is closed in} T" by auto
next
  assume pointCl:"∀x∈⋃T. {x} {is closed in} T"
  {
    fix A
    assume AS2:"A∈FinPow(⋃T)"
    let ?p="{⟨x,{x}⟩. x∈A}"
    have "?p∈A→{{x}. x∈A}" using Pi_def unfolding function_def by auto
    then have "?p:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality
      by auto
    then have "A≈{{x}. x∈A}" unfolding eqpoll_def by auto
    with AS2 have "Finite({{x}. x∈A})" unfolding FinPow_def using eqpoll_imp_Finite_iff by auto
    then have "{{x}. x∈A}∈FinPow({D ∈ Pow(⋃T) . D {is closed in} T})" using AS2 pointCl unfolding FinPow_def
    by (safe, blast+) 
    then have "(⋃{{x}. x∈A}) {is closed in} T" using fin_union_cl_is_cl by auto
    moreover
    have "⋃{{x}. x∈A}=A" by auto
    ultimately have "A {is closed in} T" by simp
  }
  then have reg:"∀A∈FinPow(⋃T). A {is closed in} T" by auto
  {
    fix U
    assume AS2:"U∈CoCardinal(⋃T,nat)"
    then have "U∈Pow(⋃T)" "U=0 ∨ ((⋃T)-U)≺nat" using CoCardinal_def by auto
    then have "U∈Pow(⋃T)" "U=0 ∨ Finite(⋃T-U)" using lesspoll_nat_is_Finite by auto
    then have "U∈Pow(⋃T)" "U∈T∨(⋃T-U) {is closed in} T" using empty_open topSpaceAssum
      reg unfolding FinPow_def by auto
    then have "U∈Pow(⋃T)" "U∈T∨(⋃T-(⋃T-U))∈T" using IsClosed_def by auto
    moreover
    then have "(⋃T-(⋃T-U))=U" by blast
    ultimately have "U∈T" by auto
  }
  then have "(CoFinite (⋃T))⊆T" using Cofinite_def by auto
  then show "T {is T⇩1}" using T1_cocardinal_coarser by auto
qed

text‹Secondly, let's show that the ‹CoCardinal X Q›
topologies for different sets $Q$ are all ordered
as the partial order of sets. (The order is linear when considering only cardinals)›

lemma order_cocardinal_top:
  fixes X
  assumes "Q1≲Q2"
  shows "CoCardinal(X,Q1) ⊆ CoCardinal(X,Q2)"
proof
  fix x
  assume "x ∈ CoCardinal(X,Q1)"
  then have "x∈Pow(X)" "x=0∨(X-x)≺Q1" using CoCardinal_def by auto
  with assms have "x∈Pow(X)" "x=0∨(X-x)≺Q2" using lesspoll_trans2 by auto
  then show "x∈CoCardinal(X,Q2)" using CoCardinal_def by auto
qed

corollary cocardinal_is_T1:
  fixes X K
  assumes "InfCard(K)"
  shows "CoCardinal(X,K) {is T⇩1}"
proof-
  have "nat≤K" using InfCard_def assms by auto
  then have "nat⊆K" using le_imp_subset by auto
  then have "nat≲K" "K≠0"using subset_imp_lepoll by auto
  then have "CoCardinal(X,nat) ⊆ CoCardinal(X,K)" "⋃CoCardinal(X,K)=X" using order_cocardinal_top 
    union_cocardinal by auto
  then show ?thesis using topology0.T1_cocardinal_coarser topology0_CoCardinal assms Cofinite_def
    by auto
qed

text‹In $T_2$-spaces, filters and nets have at most one limit point.›

lemma (in topology0) T2_imp_unique_limit_filter:
  assumes "T {is T⇩2}" "𝔉 {is a filter on}⋃T" "𝔉 →⇩F x" "𝔉 →⇩F y"
  shows "x=y"
proof-
  {
    assume "x≠y"
    from assms(3,4) have "x∈⋃T" "y∈⋃T" using FilterConverges_def assms(2)
      by auto
    with ‹x≠y› have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" using assms(1) isT2_def by auto
    then obtain U V where "x∈U" "y∈V" "U∩V=0" "U∈T" "V∈T" by auto
    then have "U∈{A∈Pow(⋃T). x∈Interior(A,T)}" "V∈{A∈Pow(⋃T). y∈Interior(A,T)}" using Top_2_L3 by auto
    then have "U∈𝔉" "V∈𝔉" using FilterConverges_def assms(2) assms(3,4)
      by auto
    then have "U∩V∈𝔉" using IsFilter_def assms(2) by auto
    with ‹U∩V=0› have "0∈𝔉" by auto
    then have "False" using IsFilter_def assms(2) by auto
  }
  then show ?thesis by auto
qed

lemma (in topology0) T2_imp_unique_limit_net:
  assumes "T {is T⇩2}" "N {is a net on}⋃T" "N →⇩N x" "N →⇩N y"
  shows "x=y"
proof-
  have "(Filter N..(⋃T)) {is a filter on} (⋃T)" "(Filter N..(⋃T)) →⇩F x" "(Filter N..(⋃T)) →⇩F y"
    using filter_of_net_is_filter(1) net_conver_filter_of_net_conver assms(2)
    assms(3,4) by auto
  with assms(1) show ?thesis using T2_imp_unique_limit_filter by auto
qed
    
text‹In fact, $T_2$-spaces are characterized by this property. For this proof we build
a filter containing the union of two filters.›

lemma (in topology0) unique_limit_filter_imp_T2:
  assumes "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩F x) ∧ (𝔉 →⇩F y)) ⟶ x=y"
  shows "T {is T⇩2}"
proof-
  {
    fix x y
    assume "x∈⋃T" "y∈⋃T" "x≠y"
    {
      assume "∀U∈T. ∀V∈T. (x∈U ∧ y∈V) ⟶ U∩V≠0"
      let ?Ux="{A∈Pow(⋃T). x∈int(A)}"
      let ?Uy="{A∈Pow(⋃T). y∈int(A)}"
      let ?FF="?Ux ∪ ?Uy ∪ {A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
      have sat:"?FF {satisfies the filter base condition}"
      proof-
        {
          fix A B
          assume "A∈?FF" "B∈?FF"
          {
            assume "A∈?Ux" 
            {
              assume "B∈?Ux"
              with ‹x∈⋃T› ‹A∈?Ux› have "A∩B∈?Ux" using neigh_filter(1) IsFilter_def by auto
              then have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈?Uy"
              with ‹A∈?Ux› have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
              with ‹x∈⋃T› ‹A∈?Ux› have "A∩B=(A∩AA)∩BB" "A∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto
              with ‹BB∈?Uy› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
              then have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          moreover
          {
            assume "A∈?Uy" 
            {
              assume "B∈?Uy"
              with ‹y∈⋃T› ‹A∈?Uy› have "A∩B∈?Uy" using neigh_filter(1) IsFilter_def by auto
              then have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈?Ux"
              with ‹A∈?Uy› have "B∩A∈?FF" by auto
              moreover have "A∩B=B∩A" by auto
              ultimately have "A∩B∈?FF" by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA BB where "B=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
              with ‹y∈⋃T› ‹A∈?Uy› have "A∩B=AA∩(A∩BB)" "A∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto
              with ‹AA∈?Ux› have "A∩B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
              then have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          moreover
          {
            assume "A∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
            then obtain AA BB where "A=AA∩BB" "AA∈?Ux" "BB∈?Uy" by auto
            {
              assume "B∈?Uy"
              with ‹BB∈?Uy› ‹y∈⋃T› have "B∩BB∈?Uy" using neigh_filter(1) IsFilter_def by auto
              moreover from ‹A=AA∩BB› have "A∩B=AA∩(B∩BB)" by auto
              ultimately have "A∩B∈?FF" using ‹AA∈?Ux› ‹B∩BB∈?Uy› by auto
            }
            moreover
            {
              assume "B∈?Ux"
              with ‹AA∈?Ux› ‹x∈⋃T› have "B∩AA∈?Ux" using neigh_filter(1) IsFilter_def by auto
              moreover from ‹A=AA∩BB› have "A∩B=(B∩AA)∩BB" by auto
              ultimately have "A∩B∈?FF" using ‹B∩AA∈?Ux› ‹BB∈?Uy› by auto
            }
            moreover
            {
              assume "B∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}"
              then obtain AA2 BB2 where "B=AA2∩BB2" "AA2∈?Ux" "BB2∈?Uy" by auto
              from ‹B=AA2∩BB2› ‹A=AA∩BB› have "A∩B=(AA∩AA2)∩(BB∩BB2)" by auto
              moreover
              from ‹AA∈?Ux›‹AA2∈?Ux›‹x∈⋃T› have "AA∩AA2∈?Ux" using neigh_filter(1) IsFilter_def by auto
              moreover
              from ‹BB∈?Uy›‹BB2∈?Uy›‹y∈⋃T› have "BB∩BB2∈?Uy" using neigh_filter(1) IsFilter_def by auto
              ultimately have "A∩B∈?FF" by auto
            }
            ultimately have "A∩B∈?FF" using ‹B∈?FF› by auto
          }
          ultimately have "A∩B∈?FF" using ‹A∈?FF› by auto
          then have "∃D∈?FF. D⊆A∩B" unfolding Bex_def by auto
        }
        then have "∀A∈?FF. ∀B∈?FF. ∃D∈?FF. D⊆A∩B" by force
        moreover
        have "⋃T∈?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto
        then have "?FF≠0" by auto
        moreover
        {
          assume "0∈?FF"
          moreover
          have "0∉?Ux" using ‹x∈⋃T› neigh_filter(1) IsFilter_def by auto
          moreover
          have "0∉?Uy" using ‹y∈⋃T› neigh_filter(1) IsFilter_def by auto
          ultimately have "0∈{A∩B. ⟨A,B⟩∈?Ux × ?Uy}" by auto
          then obtain A B where "0=A∩B" "A∈?Ux""B∈?Uy" by auto
          then have "x∈int(A)""y∈int(B)" by auto
          moreover
          with ‹0=A∩B› have "int(A)∩int(B)=0" using Top_2_L1 by auto
          moreover
          have "int(A)∈T""int(B)∈T" using Top_2_L2 by auto
          ultimately have "False" using ‹∀U∈T. ∀V∈T. x∈U∧y∈V ⟶ U∩V≠0› by auto
        }
        then have "0∉?FF" by auto
        ultimately show ?thesis using SatisfiesFilterBase_def by auto
      qed
      moreover
      have "?FF⊆Pow(⋃T)" by auto
      ultimately have bas:"?FF {is a base filter} {A∈Pow(⋃T). ∃D∈?FF. D⊆A}" "⋃{A∈Pow(⋃T). ∃D∈?FF. D⊆A}=⋃T" 
        using base_unique_filter_set2[of "?FF"] by auto
      then have fil:"{A∈Pow(⋃T). ∃D∈?FF. D⊆A} {is a filter on} ⋃T" using basic_filter sat by auto
      have "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto
      then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩F x" using convergence_filter_base2[OF fil bas(1) _ ‹x∈⋃T›] by auto
      moreover
      then have "∀U∈Pow(⋃T). y∈int(U) ⟶ (∃D∈?FF. D⊆U)" by auto
      then have "{A∈Pow(⋃T). ∃D∈?FF. D⊆A} →⇩F y" using convergence_filter_base2[OF fil bas(1) _ ‹y∈⋃T›] by auto
      ultimately have "x=y" using assms fil ‹x∈⋃T›‹y∈⋃T› by blast
      with ‹x≠y› have "False" by auto
    }
    then have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0" by blast
  }
  then show ?thesis using isT2_def by auto
qed

lemma (in topology0) unique_limit_net_imp_T2:
  assumes "∀x∈⋃T. ∀y∈⋃T. ∀N. ((N {is a net on}⋃T) ∧ (N →⇩N x) ∧ (N →⇩N y)) ⟶ x=y"
  shows "T {is T⇩2}"
proof-
  {
    fix x y 𝔉
    assume "x∈⋃T" "y∈⋃T""𝔉 {is a filter on}⋃T""𝔉 →⇩F x""𝔉 →⇩F y"
    then have "(Net(𝔉)) {is a net on} ⋃T""(Net 𝔉) →⇩N x""(Net 𝔉) →⇩N y"
      using filter_conver_net_of_filter_conver net_of_filter_is_net by auto
    with  ‹x∈⋃T› ‹y∈⋃T› have "x=y" using assms by blast
  }
  then have "∀x∈⋃T. ∀y∈⋃T. ∀𝔉. ((𝔉 {is a filter on}⋃T) ∧ (𝔉 →⇩F x) ∧ (𝔉 →⇩F y)) ⟶ x=y" by auto
  then show ?thesis using unique_limit_filter_imp_T2 by auto
qed

text‹This results make easy to check if a space is $T_2$.›

text‹The topology
which comes from a filter as in @{thm "top_of_filter"} is not $T_2$ generally.
  We will see in this file later on, that the exceptions are a consequence of the spectrum.›

corollary filter_T2_imp_card1:
  assumes "(𝔉∪{0}) {is T⇩2}" "𝔉 {is a filter on} ⋃𝔉" "x∈⋃𝔉"
  shows "⋃𝔉={x}"
proof-
  {
    fix y assume "y∈⋃𝔉"
    then have "𝔉 →⇩F y {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2) by auto
    moreover
    have "𝔉 →⇩F x {in} (𝔉∪{0})" using lim_filter_top_of_filter assms(2,3) by auto
    moreover
    have "⋃𝔉=⋃(𝔉∪{0})" by auto
    ultimately
    have "y=x" using topology0.T2_imp_unique_limit_filter[OF topology0_filter[OF assms(2)] assms(1)] assms(2)
      by auto
  }
  then have "⋃𝔉⊆{x}" by auto
  with assms(3) show ?thesis by auto
qed

text‹There are more separation axioms that just $T_0$, $T_1$ or $T_2$›

definition
  IsRegular ("_{is regular}" 90)
  where "T{is regular} ≡ ∀A. A{is closed in}T ⟶ (∀x∈⋃T-A. ∃U∈T. ∃V∈T. A⊆U∧x∈V∧U∩V=0)"

definition
  isT3 ("_{is T⇩3}" 90)
  where "T{is T⇩3} ≡ (T{is T⇩1}) ∧ (T{is regular})"

definition
  IsNormal ("_{is normal}" 90)
  where "T{is normal} ≡ ∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶
  (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))"

definition
  isT4 ("_{is T⇩4}" 90)
  where "T{is T⇩4} ≡ (T{is T⇩1}) ∧ (T{is normal})"

lemma (in topology0) T4_is_T3:
  assumes "T{is T⇩4}" shows "T{is T⇩3}"
proof-
  from assms have nor:"T{is normal}" using isT4_def by auto
  from assms have "T{is T⇩1}" using isT4_def by auto
  then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto
  {
    fix A
    assume AS:"A{is closed in}T"
    {
      fix x
      assume "x∈⋃T-A"
      have "Finite({x})" by auto
      then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto
      then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto
      then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
      with ‹x∈⋃T-A› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def 
        closed_sets_cocardinal by auto
      then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def
        by auto
      with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto
      with ‹x∈⋃T-A› have "{x}{is closed in}T" "A∩{x}=0" using IsClosed_def by auto
      with nor AS have "∃U∈T. ∃V∈T. A⊆U∧{x}⊆V∧U∩V=0" unfolding IsNormal_def by blast
      then have "∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto
    }
    then have "∀x∈⋃T-A. ∃U∈T. ∃V∈T. A⊆U∧ x∈V∧U∩V=0" by auto
  }
  then have "T{is regular}" using IsRegular_def by blast
  with ‹T{is T⇩1}› show ?thesis using isT3_def by auto
qed

lemma (in topology0) T3_is_T2:
  assumes "T{is T⇩3}" shows "T{is T⇩2}"
proof-
  from assms have "T{is regular}" using isT3_def by auto
  from assms have "T{is T⇩1}" using isT3_def by auto
  then have "Cofinite (⋃T)⊆T" using T1_cocardinal_coarser by auto
  {
    fix x y
    assume "x∈⋃T""y∈⋃T""x≠y"
    have "Finite({x})" by auto
    then obtain n where "{x}≈n" "n∈nat" unfolding Finite_def by auto
    then have "{x}≲n" "n∈nat" using eqpoll_imp_lepoll by auto
    then have "{x}≺nat" using n_lesspoll_nat lesspoll_trans1 by auto
    with ‹x∈⋃T› have "{x} {is closed in} (Cofinite (⋃T))" using Cofinite_def 
      closed_sets_cocardinal by auto
    then have "⋃T-{x}∈Cofinite(⋃T)" unfolding IsClosed_def using union_cocardinal Cofinite_def
       by auto
    with ‹Cofinite (⋃T)⊆T› have "⋃T-{x}∈T" by auto
    with ‹x∈⋃T›‹y∈⋃T›‹x≠y› have "{x}{is closed in}T" "y∈⋃T-{x}" using IsClosed_def by auto
    with ‹T{is regular}› have "∃U∈T. ∃V∈T. {x}⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by force
    then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" by auto
  }
  then show ?thesis using isT2_def by auto
qed

text‹Regularity can be rewritten in terms of existence of certain neighboorhoods.›

lemma (in topology0) regular_imp_exist_clos_neig:
  assumes "T{is regular}" and "U∈T" and "x∈U"
  shows "∃V∈T. x∈V ∧ cl(V)⊆U"
proof-
  from assms(2) have "(⋃T-U){is closed in}T" using Top_3_L9 by auto moreover
  from assms(2,3) have "x∈⋃T" by auto moreover
  note assms(1,3) ultimately obtain A B where "A∈T" and "B∈T" and "A∩B=0" and "(⋃T-U)⊆A" and "x∈B"
    unfolding IsRegular_def by blast
  from ‹A∩B=0› ‹B∈T› have "B⊆⋃T-A" by auto
  with ‹A∈T› have "cl(B)⊆⋃T-A" using Top_3_L9 Top_3_L13 by auto
  moreover from ‹(⋃T-U)⊆A› assms(3) have "⋃T-A⊆U" by auto
  moreover note ‹x∈B› ‹B∈T›
  ultimately have "B∈T ∧ x∈B ∧ cl(B)⊆U" by auto
  then show ?thesis by auto
qed

lemma (in topology0) exist_clos_neig_imp_regular:
  assumes "∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U)"
  shows "T{is regular}"
proof-
  {
    fix F
    assume "F{is closed in}T" 
    {
      fix x assume "x∈⋃T-F"
      with ‹F{is closed in}T› have "x∈⋃T" "⋃T-F∈T" "F⊆⋃T" unfolding IsClosed_def by auto
      with assms ‹x∈⋃T-F› have "∃V∈T. x∈V ∧ cl(V)⊆⋃T-F" by auto
      then obtain V where "V∈T" "x∈V" "cl(V)⊆⋃T-F" by auto
      from ‹cl(V)⊆⋃T-F› ‹F⊆⋃T› have "F⊆⋃T-cl(V)" by auto
      moreover from ‹V∈T› have "⋃T-(⋃T-V)=V" by auto
      then have "cl(V)=⋃T-int(⋃T-V)" using Top_3_L11(2)[of "⋃T-V"] by auto
      ultimately have "F⊆int(⋃T-V)" by auto moreover
      have "int(⋃T-V)⊆⋃T-V" using Top_2_L1 by auto
      then have "V∩(int(⋃T-V))=0" by auto moreover
      note ‹x∈V›‹V∈T› ultimately
      have "V∈T" "int(⋃T-V)∈T" "F⊆int(⋃T-V) ∧ x∈V ∧ (int(⋃T-V))∩V=0" using Top_2_L2
        by auto
      then have "∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto
    }
    then have "∀x∈⋃T-F. ∃U∈T. ∃V∈T. F⊆U ∧ x∈V ∧ U∩V=0" by auto
  }
  then show ?thesis using IsRegular_def by blast
qed

lemma (in topology0) regular_eq:
  shows "T{is regular} ⟷ (∀x∈⋃T. ∀U∈T. x∈U ⟶ (∃V∈T. x∈V∧ cl(V)⊆U))"
  using regular_imp_exist_clos_neig exist_clos_neig_imp_regular by force

text‹A Hausdorff space separates compact spaces from points.›

theorem (in topology0) T2_compact_point:
  assumes "T{is T⇩2}" "A{is compact in}T" "x∈⋃T" "x∉A"
  shows "∃U∈T. ∃V∈T. A⊆U ∧ x∈V ∧ U∩V=0"
proof-
  {
    assume "A=0"
    then have "A⊆0∧x∈⋃T∧(0∩(⋃T)=0)" using assms(3) by auto 
    then have ?thesis using empty_open topSpaceAssum unfolding IsATopology_def by auto
  }
  moreover
  {
    assume noEmpty:"A≠0"
    let ?U="{⟨U,V⟩∈T×T. x∈U∧U∩V=0}"
    {
      fix y assume "y∈A"
      with ‹x∉A› assms(4) have "x≠y" by auto
      moreover from ‹y∈A› have "x∈⋃T""y∈⋃T" using assms(2,3) unfolding IsCompact_def by auto
      ultimately obtain U V where "U∈T""V∈T""U∩V=0""x∈U""y∈V" using assms(1) unfolding isT2_def by blast
      then have "∃⟨U,V⟩∈?U. y∈V" by auto
    }
    then have "∀y∈A. ∃⟨U,V⟩∈?U. y∈V" by auto
    then have "A⊆⋃{snd(B). B∈?U}" by auto
    moreover have "{snd(B). B∈?U}∈Pow(T)" by auto
    ultimately have "∃N∈FinPow({snd(B). B∈?U}). A⊆⋃N" using assms(2) unfolding IsCompact_def by auto
    then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "A⊆⋃N" by auto
    with ‹{snd(B). B∈?U}∈Pow(T)› have "A⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto
    then have NN:"A⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto
    from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def 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
    from noEmpty ‹A⊆⋃N› have NnoEmpty:"N≠0" by auto
    let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}"
    have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto
    {
      fix n assume "n∈N"
      with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto
      then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto
      then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover
      from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto
      with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto
      ultimately have "?QQ`n≠0" by auto
    }
    then have "∀n∈N. ?QQ`n≠0" by auto
    with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def
      by auto
    then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto
    from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast)
    {
      fix t assume "t∈N"
      then have "f`t∈?QQ`t" using fPI(2) by auto
      with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto
    }
    then have reg:"∀t∈N. f`t∈⋃(?QQ``N)"  "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto
    {
      fix tt assume "tt∈f"
      with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto
      then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto
      then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto
      with reg(2) have "y∈⋃(?QQ``N)" by blast
      with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto
      then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto
    }
    then have ffun:"f:N→⋃(?QQ``N)"  using fPI(1) unfolding Pi_def by auto
    then have "f∈surj(N,range(f))" using fun_is_surj by auto
    with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto
    with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast
    with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto
    moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto
    then have "range(f)⊆T" by auto
    ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto
    then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover
    {
      fix S assume "S∈range(f)"
      with rr have "S∈⋃(?QQ``N)" by blast
      then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto
      then obtain B where "B∈(?QQ``N)" "S∈B" by auto
      then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto
      then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto
      with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto
      then have "x∈S" by auto
    }
    then have "x∈⋂range(f)" using ‹range(f)≠0› by auto moreover
    {
      fix y assume "y∈(⋃N)∩(⋂range(f))"
      then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto
      then obtain t where "t∈N" "y∈t" by auto
      then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto
      then have "f`t∈range(f)" using apply_rangeI ffun by auto
      with reg have yft:"y∈f`t" by auto
      with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto
      with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto
      then have "⟨f`t,t⟩∈?U" by auto
      then have "f`t∩t=0" by auto
      with ‹y∈t› yft have "False" by auto
    }
    then have "(⋃N)∩(⋂range(f))=0" by blast moreover
    note NN
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed

text‹A Hausdorff space separates compact spaces from other compact spaces.›

theorem (in topology0) T2_compact_compact:
  assumes "T{is T⇩2}" "A{is compact in}T" "B{is compact in}T" "A∩B=0"
  shows "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0"
proof-
 {
    assume "B=0"
    then have "A⊆⋃T∧B⊆0∧((⋃T)∩0=0)" using assms(2) unfolding IsCompact_def by auto moreover
    have "0∈T" using empty_open topSpaceAssum by auto moreover
    have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately
    have ?thesis by auto
  }
  moreover
  {
    assume noEmpty:"B≠0"
    let ?U="{⟨U,V⟩∈T×T. A⊆U ∧ U∩V=0}"
    {
      fix y assume "y∈B"
      then have "y∈⋃T" using assms(3) unfolding IsCompact_def by auto
      with ‹y∈B› have "∃U∈T. ∃V∈T. A⊆U ∧ y∈V ∧ U∩V=0" using T2_compact_point assms(1,2,4) by auto
      then have "∃⟨U,V⟩∈?U. y∈V" by auto
    }
    then have "∀y∈B. ∃⟨U,V⟩∈?U. y∈V" by auto
    then have "B⊆⋃{snd(B). B∈?U}" by auto
    moreover have "{snd(B). B∈?U}∈Pow(T)" by auto
    ultimately have "∃N∈FinPow({snd(B). B∈?U}). B⊆⋃N" using assms(3) unfolding IsCompact_def by auto
    then obtain N where ss:"N∈FinPow({snd(B). B∈?U})" "B⊆⋃N" by auto
    with ‹{snd(B). B∈?U}∈Pow(T)› have "B⊆⋃N" "N∈Pow(T)" unfolding FinPow_def by auto
    then have NN:"B⊆⋃N" "⋃N∈T" using topSpaceAssum unfolding IsATopology_def by auto
    from ss have "Finite(N)""N⊆{snd(B). B∈?U}" unfolding FinPow_def 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
    from noEmpty ‹B⊆⋃N› have NnoEmpty:"N≠0" by auto
    let ?QQ="{⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩. n∈N}"
    have QQPi:"?QQ:N→{{fst(B). B∈{A∈?U. snd(A)=n}}. n∈N}" unfolding Pi_def function_def domain_def by auto
    {
      fix n assume "n∈N"
      with ‹N⊆{snd(B). B∈?U}› obtain B where "n=snd(B)" "B∈?U" by auto
      then have "fst(B)∈{fst(B). B∈{A∈?U. snd(A)=n}}" by auto
      then have "{fst(B). B∈{A∈?U. snd(A)=n}}≠0" by auto moreover
      from ‹n∈N› have "⟨n,{fst(B). B∈{A∈?U. snd(A)=n}}⟩∈?QQ" by auto
      with QQPi have "?QQ`n={fst(B). B∈{A∈?U. snd(A)=n}}" using apply_equality by auto
      ultimately have "?QQ`n≠0" by auto
    }
    then have "∀n∈N. ?QQ`n≠0" by auto
    with ‹n∈nat› ‹N≲n› have "∃f. f∈Pi(N,λt. ?QQ`t) ∧ (∀t∈N. f`t∈?QQ`t)" using finite_choice unfolding AxiomCardinalChoiceGen_def
      by auto
    then obtain f where fPI:"f∈Pi(N,λt. ?QQ`t)" "(∀t∈N. f`t∈?QQ`t)" by auto
    from fPI(1) NnoEmpty have "range(f)≠0" unfolding Pi_def range_def domain_def converse_def by (safe,blast)
    {
      fix t assume "t∈N"
      then have "f`t∈?QQ`t" using fPI(2) by auto
      with ‹t∈N› have "f`t∈⋃(?QQ``N)" "?QQ`t⊆⋃(?QQ``N)" using func_imagedef QQPi by auto
    }
    then have reg:"∀t∈N. f`t∈⋃(?QQ``N)"  "∀t∈N. ?QQ`t⊆⋃(?QQ``N)" by auto
    {
      fix tt assume "tt∈f"
      with fPI(1) have "tt∈Sigma(N, (`)(?QQ))" unfolding Pi_def by auto
      then have "tt∈(⋃xa∈N. ⋃y∈?QQ`xa. {⟨xa,y⟩})" unfolding Sigma_def by auto
      then obtain xa y where "xa∈N" "y∈?QQ`xa" "tt=⟨xa,y⟩" by auto
      with reg(2) have "y∈⋃(?QQ``N)" by blast
      with ‹tt=⟨xa,y⟩› ‹xa∈N› have "tt∈(⋃xa∈N. ⋃y∈⋃(?QQ``N). {⟨xa,y⟩})" by auto
      then have "tt∈N×(⋃(?QQ``N))" unfolding Sigma_def by auto
    }
    then have ffun:"f:N→⋃(?QQ``N)"  using fPI(1) unfolding Pi_def by auto
    then have "f∈surj(N,range(f))" using fun_is_surj by auto
    with ‹N≲n› ‹n∈nat› have "range(f)≲N" using surj_fun_inv_2 nat_into_Ord by auto
    with ‹N≲n› have "range(f)≲n" using lepoll_trans by blast
    with ‹n∈nat› have "Finite(range(f))" using n_lesspoll_nat lesspoll_nat_is_Finite lesspoll_trans1 by auto
    moreover from ffun have rr:"range(f)⊆⋃(?QQ``N)" unfolding Pi_def by auto
    then have "range(f)⊆T" by auto
    ultimately have "range(f)∈FinPow(T)" unfolding FinPow_def by auto
    then have "⋂range(f)∈T" using fin_inter_open_open ‹range(f)≠0› by auto moreover
    {
      fix S assume "S∈range(f)"
      with rr have "S∈⋃(?QQ``N)" by blast
      then have "∃B∈(?QQ``N). S ∈ B" using Union_iff by auto
      then obtain B where "B∈(?QQ``N)" "S∈B" by auto
      then have "∃rr∈N. ⟨rr,B⟩∈?QQ" unfolding image_def by auto
      then have "∃rr∈N. B={fst(B). B∈{A∈?U. snd(A)=rr}}" by auto
      with ‹S∈B› obtain rr where "⟨S,rr⟩∈?U" by auto
      then have "A⊆S" by auto
    }
    then have "A⊆⋂range(f)" using ‹range(f)≠0› by auto moreover
    {
      fix y assume "y∈(⋃N)∩(⋂range(f))"
      then have reg:"(∀S∈range(f). y∈S)∧(∃t∈N. y∈t)" by auto
      then obtain t where "t∈N" "y∈t" by auto
      then have "⟨t, {fst(B). B∈{A∈?U. snd(A)=t}}⟩∈?QQ" by auto
      then have "f`t∈range(f)" using apply_rangeI ffun by auto
      with reg have yft:"y∈f`t" by auto
      with ‹t∈N› fPI(2) have "f`t∈?QQ`t" by auto
      with ‹t∈N› have "f`t∈{fst(B). B∈{A∈?U. snd(A)=t}}" using apply_equality QQPi by auto
      then have "⟨f`t,t⟩∈?U" by auto
      then have "f`t∩t=0" by auto
      with ‹y∈t› yft have "False" by auto
    }
    then have "(⋂range(f))∩(⋃N)=0" by blast moreover
    note NN
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed

text‹A compact Hausdorff space is normal.›

corollary (in topology0) T2_compact_is_normal:
  assumes "T{is T⇩2}" "(⋃T){is compact in}T"
  shows "T{is normal}" unfolding IsNormal_def
proof-
  from assms(2) have car_nat:"(⋃T){is compact of cardinal}nat{in}T" using Compact_is_card_nat by auto
  {
    fix A B assume "A{is closed in}T" "B{is closed in}T""A∩B=0"
    then have com:"((⋃T)∩A){is compact of cardinal}nat{in}T" "((⋃T)∩B){is compact of cardinal}nat{in}T" using compact_closed[OF car_nat] 
      by auto
    from ‹A{is closed in}T›‹B{is closed in}T› have "(⋃T)∩A=A""(⋃T)∩B=B" unfolding IsClosed_def by auto
    with com have "A{is compact of cardinal}nat{in}T" "B{is compact of cardinal}nat{in}T" by auto
    then have "A{is compact in}T""B{is compact in}T" using Compact_is_card_nat by auto
    with ‹A∩B=0› have "∃U∈T. ∃V∈T. A⊆U ∧ B⊆V ∧ U∩V=0" using T2_compact_compact assms(1) by auto
  }
  then show " ∀A. A {is closed in} T ⟶ (∀B. B {is closed in} T ∧ A ∩ B = 0 ⟶ (∃U∈T. ∃V∈T. A ⊆ U ∧ B ⊆ V ∧ U ∩ V = 0))"
    by auto
qed

subsection‹Hereditability›

text‹A topological property is hereditary if whenever a space has it, 
every subspace also has it.›

definition IsHer ("_{is hereditary}" 90)
  where "P {is hereditary} ≡ ∀T. T{is a topology} ∧ P(T) ⟶ (∀A∈Pow(⋃T). P(T{restricted to}A))"

lemma subspace_of_subspace:
  assumes "A⊆B""B⊆⋃T"
  shows "T{restricted to}A=(T{restricted to}B){restricted to}A"
proof
  from assms have S:"∀S∈T. A∩(B∩S)=A∩S" by auto
  then show "T {restricted to} A ⊆ T {restricted to} B {restricted to} A" unfolding RestrictedTo_def
    by auto
  from S show "T {restricted to} B {restricted to} A ⊆ T {restricted to} A" unfolding RestrictedTo_def
    by auto
qed
 
text‹The separation properties $T_0$, $T_1$, $T_2$ y $T_3$ are hereditary.›

theorem regular_here:
  assumes "T{is regular}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is regular}"
proof-
  {
    fix C
    assume A:"C{is closed in}(T{restricted to}A)"
    {fix y assume "y∈⋃(T{restricted to}A)""y∉C"
    with A have "(⋃(T{restricted to}A))-C∈(T{restricted to}A)""C⊆⋃(T{restricted to}A)" "y∈⋃(T{restricted to}A)""y∉C" unfolding IsClosed_def
      by auto
    moreover
    with assms(2) have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
    ultimately have "A-C∈T{restricted to}A" "y∈A""y∉C""C∈Pow(A)" by auto
    then obtain S where "S∈T" "A∩S=A-C" "y∈A""y∉C" unfolding RestrictedTo_def by auto
    then have "y∈A-C""A∩S=A-C" by auto
    with ‹C∈Pow(A)› have "y∈A∩S""C=A-A∩S" by auto
    then have "y∈S" "C=A-S" by auto
    with assms(2) have "y∈S" "C⊆⋃T-S" by auto
    moreover
    from ‹S∈T› have "⋃T-(⋃T-S)=S" by auto
    moreover
    with ‹S∈T› have "(⋃T-S) {is closed in}T" using IsClosed_def by auto
    ultimately have "y∈⋃T-(⋃T-S)" "(⋃T-S) {is closed in}T" by auto
    with assms(1) have "∀y∈⋃T-(⋃T-S). ∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" unfolding IsRegular_def by auto
    with ‹y∈⋃T-(⋃T-S)› have "∃U∈T. ∃V∈T. (⋃T-S)⊆U∧y∈V∧U∩V=0" by auto
    then obtain U V where "U∈T""V∈T" "⋃T-S⊆U""y∈V""U∩V=0" by auto
    then have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "C⊆U""y∈V""(A∩U)∩(A∩V)=0"
      unfolding RestrictedTo_def  using ‹C⊆⋃T-S› by auto
    moreover
    with ‹C∈Pow(A)›‹y∈A› have "C⊆A∩U""y∈A∩V" by auto
    ultimately have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧y∈V∧U∩V=0" by auto
  }
    then have "∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0" by auto
  }
  then have "∀C. C{is closed in}(T{restricted to}A) ⟶ (∀x∈⋃(T{restricted to}A)-C. ∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). C⊆U∧x∈V∧U∩V=0)"
   by blast
  then show ?thesis using IsRegular_def by auto
qed

corollary here_regular:
  shows "IsRegular {is hereditary}" using regular_here IsHer_def by auto

theorem T1_here:
  assumes "T{is T⇩1}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩1}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. x∈U∧y∉U" using assms(1) isT1_def by auto
    then obtain U where "U∈T""x∈U""y∉U" by auto
    with ‹x∈A› have "A∩U∈(T{restricted to}A)" "x∈A∩U" "y∉A∩U" unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). x∈U∧y∉U" by blast
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). x∈U∧y∉U)"
    by auto
  then show ?thesis using isT1_def by auto
qed

corollary here_T1:
  shows "isT1 {is hereditary}" using T1_here IsHer_def by auto

lemma here_and:
  assumes "P {is hereditary}" "Q {is hereditary}"
  shows "(λT. P(T) ∧ Q(T)) {is hereditary}" using assms unfolding IsHer_def by auto

corollary here_T3:
  shows "isT3 {is hereditary}" using here_and[OF here_T1 here_regular] unfolding IsHer_def isT3_def.

lemma T2_here:
  assumes "T{is T⇩2}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩2}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. ∃V∈T. x∈U∧y∈V∧U∩V=0" using assms(1) isT2_def by auto
    then obtain U V where "U∈T" "V∈T""x∈U""y∈V""U∩V=0" by auto
    with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)""A∩V∈(T{restricted to}A)" "x∈A∩U" "y∈A∩V" "(A∩U)∩(A∩V)=0"unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0" unfolding Bex_def by auto
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). ∃V∈(T{restricted to}A). x∈U∧y∈V∧U∩V=0)"
    by auto
  then show ?thesis using isT2_def by auto
qed

corollary here_T2:
  shows "isT2 {is hereditary}" using T2_here IsHer_def by auto

lemma T0_here:
  assumes "T{is T⇩0}" "A∈Pow(⋃T)" shows "(T{restricted to}A){is T⇩0}"
proof-
  from assms(2) have un:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  {
    fix x y
    assume "x∈A""y∈A""x≠y"
    with ‹A∈Pow(⋃T)› have "x∈⋃T""y∈⋃T""x≠y" by auto
    then have "∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U)" using assms(1) isT0_def by auto
    then obtain U where "U∈T" "(x∈U∧y∉U)∨(y∈U∧x∉U)" by auto
    with ‹x∈A›‹y∈A› have "A∩U∈(T{restricted to}A)" "(x∈A∩U∧y∉A∩U)∨(y∈A∩U∧x∉A∩U)" unfolding RestrictedTo_def by auto
    then have "∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U)" unfolding Bex_def by auto
  }
  with un have "∀x y. x∈⋃(T{restricted to}A) ∧ y∈⋃(T{restricted to}A) ∧ x≠y ⟶ (∃U∈(T{restricted to}A). (x∈U∧y∉U)∨(y∈U∧x∉U))"
    by auto
  then show ?thesis using isT0_def by auto
qed

corollary here_T0:
  shows "isT0 {is hereditary}" using T0_here IsHer_def by auto

subsection‹Spectrum and anti-properties›

text‹The spectrum of a topological property is a class of
sets such that all topologies defined over that set have that property.›

text‹The spectrum of a property gives us the list of sets for which the property doesn't give
any topological information. Being in the spectrum of a topological property is an invariant
in the category of sets and function; mening that equipollent sets are in the same
spectra.›
      
definition Spec ("_ {is in the spectrum of} _" 99)
  where "Spec(K,P) ≡ ∀T. ((T{is a topology} ∧ ⋃T≈K) ⟶ P(T))"

lemma equipollent_spect:
  assumes "A≈B" "B {is in the spectrum of} P"
  shows  "A {is in the spectrum of} P"
proof-
  from assms(2) have "∀T. ((T{is a topology} ∧ ⋃T≈B) ⟶ P(T))" using Spec_def by auto
  then have "∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ P(T))" using eqpoll_trans[OF _ assms(1)] by auto
  then show ?thesis using Spec_def by auto
qed

theorem eqpoll_iff_spec:
  assumes "A≈B"
  shows "(B {is in the spectrum of} P) ⟷ (A {is in the spectrum of} P)"
proof
  assume "B {is in the spectrum of} P"
  with assms equipollent_spect show "A {is in the spectrum of} P" by auto
next
  assume "A {is in the spectrum of} P"
  moreover
  from assms have "B≈A" using eqpoll_sym by auto
  ultimately show "B {is in the spectrum of} P" using equipollent_spect by auto
qed

text‹From the previous statement, we see that the spectrum could be formed only by
representative of clases of sets. If \emph{AC} holds, this means that the spectrum
can be taken as a set or class of cardinal numbers.›

text‹Here is an example of the spectrum. The proof lies in the indiscrite filter ‹{A}›
that can be build for any set. In this proof, we see that without choice,
there is no way to define the sepctrum of a property with cardinals because if a set is not 
comparable with any ordinal, its cardinal is defined as ‹0› without the set being
empty.›

theorem T4_spectrum:
  shows "(A {is in the spectrum of} isT4) ⟷ A ≲ 1"
proof
  assume "A {is in the spectrum of} isT4"
  then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩4}))" using Spec_def by auto
  {
    assume "A≠0"
    then obtain x where "x∈A" by auto
    then have "x∈⋃{A}" by auto
    moreover
    then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto
    moreover
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto
    then have top:"({A}∪{0}) {is a topology}" "⋃({A}∪{0})≈A" using eqpoll_refl by auto
    then have "({A}∪{0}) {is T⇩4}" using reg by auto
    then have "({A}∪{0}) {is T⇩2}" using topology0.T3_is_T2 topology0.T4_is_T3 topology0_def top by auto
    ultimately have "⋃{A}={x}" using filter_T2_imp_card1[of "{A}""x"] by auto
    then have "A={x}" by auto
    then have "A≈1" using singleton_eqpoll_1 by auto
  }
  moreover
  have "A=0 ⟶ A≈0" by auto
  ultimately have "A≈1∨A≈0" by blast
  then show "A≲1" using empty_lepollI eqpoll_imp_lepoll eq_lepoll_trans by auto
next
  assume "A≲1"
  have "A=0∨A≠0" by auto
  then obtain E where "A=0∨E∈A" by auto
  then have "A≈0∨E∈A" by auto
  with ‹A≲1› have "A≈0∨A={E}" using lepoll_1_is_sing by auto
  then have "A≈0∨A≈1" using singleton_eqpoll_1 by auto
  {
    fix T
    assume AS:"T{is a topology}""⋃T≈A"
    {
      assume "A≈0"
      with AS have "T{is a topology}" and empty:"⋃T=0" using eqpoll_trans eqpoll_0_is_0 by auto
      then have "T{is T⇩2}" using isT2_def by auto
      then have "T{is T⇩1}" using T2_is_T1 by auto
      moreover
      from empty have "T⊆{0}" by auto
      with AS(1) have "T={0}" using empty_open by auto
      from empty have rr:"∀A. A{is closed in}T ⟶ A=0" using IsClosed_def by auto
      have "∃U∈T. ∃V∈T. 0⊆U∧0⊆V∧U∩V=0" using empty_open AS(1) by auto
      with rr have "∀A. A{is closed in}T ⟶ (∀B. B{is closed in}T ∧ A∩B=0 ⟶ (∃U∈T. ∃V∈T. A⊆U∧B⊆V∧U∩V=0))"
        by blast
      then have "T{is normal}" using IsNormal_def by auto
      with ‹T{is T⇩1}› have "T{is T⇩4}" using isT4_def by auto
    }
    moreover
    {
      assume "A≈1"
      with AS have "T{is a topology}" and NONempty:"⋃T≈1" using eqpoll_trans[of "⋃T""A""1"] by auto
      then have "⋃T≲1" using eqpoll_imp_lepoll by auto
      moreover
      {
        assume "⋃T=0"
        then have "0≈⋃T" by auto
        with NONempty have "0≈1" using eqpoll_trans by blast
        then have "0=1" using eqpoll_0_is_0 eqpoll_sym by auto
        then have "False" by auto
      }
      then have "⋃T≠0" by auto
      then obtain R where "R∈⋃T" by blast
      ultimately have "⋃T={R}" using lepoll_1_is_sing by auto
      {
        fix x y
        assume "x{is closed in}T""y{is closed in}T" "x∩y=0"
        then have "x⊆⋃T""y⊆⋃T" using IsClosed_def by auto
        then have "x=0∨y=0" using ‹x∩y=0› ‹⋃T={R}› by force
        {
          assume "x=0"
          then have "x⊆0""y⊆⋃T" using ‹y⊆⋃T› by auto
          moreover
          have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto
          ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto
        }
        moreover
        {
          assume "x≠0"
          with ‹x=0∨y=0› have "y=0" by auto
          then have "x⊆⋃T""y⊆0" using ‹x⊆⋃T› by auto
          moreover
          have "0∈T""⋃T∈T" using AS(1) IsATopology_def empty_open by auto
          ultimately have "∃U∈T. ∃V∈T. x⊆U∧y⊆V∧U∩V=0" by auto
        }
        ultimately
        have "(∃U∈T. ∃V∈T. x ⊆ U ∧ y ⊆ V ∧ U ∩ V = 0)" by blast
      }
      then have "T{is normal}" using IsNormal_def by auto
      moreover
      {
        fix x y
        assume "x∈⋃T""y∈⋃T""x≠y"
        with ‹⋃T={R}› have "False" by auto
        then have "∃U∈T. x∈U∧y∉U" by auto
      }
      then have "T{is T⇩1}" using isT1_def by auto
      ultimately have "T{is T⇩4}" using isT4_def by auto
    }
    ultimately have "T{is T⇩4}" using ‹A≈0∨A≈1› by auto
  }
  then have "∀T. (T{is a topology} ∧ ⋃T ≈ A) ⟶ (T{is T⇩4})" by auto
  then show "A {is in the spectrum of} isT4" using Spec_def by auto
qed

text‹If the topological properties are related, then so are the spectra.›
    
lemma P_imp_Q_spec_inv:
  assumes "∀T. T{is a topology} ⟶ (Q(T) ⟶ P(T))"  "A {is in the spectrum of} Q"
  shows "A {is in the spectrum of} P"
proof-
  from assms(2) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ Q(T)" using Spec_def by auto
  with assms(1) have "∀T. T{is a topology} ∧ ⋃T ≈ A ⟶ P(T)" by auto
  then show ?thesis using Spec_def by auto
qed

text‹Since we already now the spectrum of $T_4$; if we now the spectrum of $T_0$,
it should be easier to compute the spectrum of $T_1$, $T_2$ and $T_3$.›

theorem T0_spectrum:
  shows "(A {is in the spectrum of} isT0) ⟷ A ≲ 1"
proof
  assume "A {is in the spectrum of} isT0"
  then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ (T {is T⇩0}))" using Spec_def by auto
  {
    assume "A≠0"
    then obtain x where "x∈A" by auto
    then have "x∈⋃{A}" by auto
    moreover
    then have "{A} {is a filter on}⋃{A}" using IsFilter_def by auto
    moreover
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})=A" using top_of_filter by auto
    then have "({A}∪{0}) {is a topology} ∧ ⋃({A}∪{0})≈A" using eqpoll_refl by auto
    then have "({A}∪{0}) {is T⇩0}" using reg by auto
    {
      fix y
      assume "y∈A""x≠y"
      with ‹({A}∪{0}) {is T⇩0}› obtain U where "U∈({A}∪{0})" and dis:"(x ∈ U ∧ y ∉ U) ∨ (y ∈ U ∧ x ∉ U)" using isT0_def by auto
      then have "U=A" by auto
      with dis ‹y∈A› ‹x∈⋃{A}› have "False" by auto
    }
    then have "∀y∈A. y=x" by auto
    with ‹x∈⋃{A}› have "A={x}" by blast
    then have "A≈1" using singleton_eqpoll_1 by auto
  }
  moreover
  have "A=0 ⟶ A≈0" by auto
  ultimately have "A≈1∨A≈0" by blast
  then show "A≲1" using empty_lepollI eqpoll_imp_lepoll eq_lepoll_trans by auto
next
  assume "A≲1"
  {
    fix T
    assume "T{is a topology}"
    then have "(T{is T⇩4})⟶(T{is T⇩0})" using topology0.T4_is_T3 topology0.T3_is_T2 T2_is_T1 T1_is_T0 
      topology0_def by auto
  }
  then have "∀T. T{is a topology} ⟶ ((T{is T⇩4})⟶(T{is T⇩0}))" by auto
  then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT0)"
    using P_imp_Q_spec_inv[of "λT. (T{is T⇩4})""λT. T{is T⇩0}"] by auto
  then show "(A {is in the spectrum of} isT0)" using T4_spectrum ‹A≲1› by auto
qed

theorem T1_spectrum:
  shows "(A {is in the spectrum of} isT1) ⟷ A ≲ 1"
proof-
  note T2_is_T1 topology0.T3_is_T2 topology0.T4_is_T3
  then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT1)"
    using P_imp_Q_spec_inv[of "isT4""isT1"] topology0_def by auto
  moreover
  note T1_is_T0
  then have "(A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of}isT0)"
    using P_imp_Q_spec_inv[of "isT1""isT0"] by auto
  moreover
  note T0_spectrum T4_spectrum
  ultimately show ?thesis by blast
qed

theorem T2_spectrum:
  shows "(A {is in the spectrum of} isT2) ⟷ A ≲ 1"
proof-
  note topology0.T3_is_T2 topology0.T4_is_T3
  then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT2)"
    using P_imp_Q_spec_inv[of "isT4""isT2"] topology0_def by auto
  moreover
  note T2_is_T1
  then have "(A {is in the spectrum of} isT2) ⟶ (A {is in the spectrum of}isT1)"
    using P_imp_Q_spec_inv[of "isT2""isT1"] by auto
  moreover
  note T1_spectrum T4_spectrum
  ultimately show ?thesis by blast
qed

theorem T3_spectrum:
  shows "(A {is in the spectrum of} isT3) ⟷ A ≲ 1"
proof-
  note topology0.T4_is_T3
  then have "(A {is in the spectrum of} isT4) ⟶ (A {is in the spectrum of} isT3)"
    using P_imp_Q_spec_inv[of "isT4""isT3"] topology0_def by auto
  moreover
  note topology0.T3_is_T2
  then have "(A {is in the spectrum of} isT3) ⟶ (A {is in the spectrum of}isT2)"
    using P_imp_Q_spec_inv[of "isT3""isT2"] topology0_def by auto
  moreover
  note T2_spectrum T4_spectrum
  ultimately show ?thesis by blast
qed

theorem compact_spectrum:
  shows "(A {is in the spectrum of} (λT. (⋃T) {is compact in}T)) ⟷ Finite(A)"
proof
  assume "A {is in the spectrum of} (λT. (⋃T) {is compact in}T)"
  then have reg:"∀T. T{is a topology} ∧ ⋃T≈A ⟶ ((⋃T) {is compact in}T)" using Spec_def by auto
  have "Pow(A){is a topology} ∧ ⋃Pow(A)=A" using Pow_is_top by auto
  then have "Pow(A){is a topology} ∧ ⋃Pow(A)≈A" using eqpoll_refl by auto
  with reg have "A{is compact in}Pow(A)" by auto
  moreover
  have "{{x}. x∈A}∈Pow(Pow(A))" by auto
  moreover
  have "⋃{{x}. x∈A}=A" by auto
  ultimately have "∃N∈FinPow({{x}. x∈A}). A⊆⋃N" using IsCompact_def by auto
  then obtain N where "N∈FinPow({{x}. x∈A})" "A⊆⋃N" by auto
  then have "N⊆{{x}. x∈A}" "Finite(N)" "A⊆⋃N" using FinPow_def by auto
  {
    fix t
    assume "t∈{{x}. x∈A}"
    then obtain x where "x∈A""t={x}" by auto
    with ‹A⊆⋃N› have "x∈⋃N" by auto
    then obtain B where "B∈N""x∈B" by auto
    with ‹N⊆{{x}. x∈A}› have "B={x}" by auto
    with ‹t={x}›‹B∈N› have "t∈N" by auto 
  }
  with ‹N⊆{{x}. x∈A}› have "N={{x}. x∈A}" by auto
  with ‹Finite(N)› have "Finite({{x}. x∈A})" by auto
  let ?B="{⟨x,{x}⟩. x∈A}"
  have "?B:A→{{x}. x∈A}" unfolding Pi_def function_def by auto
  then have "?B:bij(A,{{x}. x∈A})" unfolding bij_def inj_def surj_def using apply_equality by auto
  then have "A≈{{x}. x∈A}" using eqpoll_def by auto
  with ‹Finite({{x}. x∈A})› show "Finite(A)" using eqpoll_imp_Finite_iff by auto
next
  assume "Finite(A)"
  {
    fix T assume "T{is a topology}" "⋃T≈A"
    with ‹Finite(A)› have "Finite(⋃T)" using eqpoll_imp_Finite_iff by auto
    then have "Finite(Pow(⋃T))" using Finite_Pow by auto
    moreover
    have "T⊆Pow(⋃T)" by auto
    ultimately have "Finite(T)" using subset_Finite by auto
    {
      fix M
      assume "M∈Pow(T)""⋃T⊆⋃M"
      with ‹Finite(T)› have "Finite(M)" using subset_Finite by auto
      with ‹⋃T⊆⋃M› have "∃N∈FinPow(M). ⋃T⊆⋃N" using FinPow_def by auto
    }
    then have "(⋃T){is compact in}T" unfolding IsCompact_def by auto
  }
  then show "A {is in the spectrum of} (λT. (⋃T) {is compact in}T)" using Spec_def by auto
qed

text‹It is, at least for some people, surprising that the spectrum of some properties cannot be completely
determined in \emph{ZF}.›

theorem compactK_spectrum:
  assumes "{the axiom of}K{choice holds for subsets}(Pow(K))" "Card(K)"
  shows "(A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))) ⟷ (A≲K)"
proof
  assume "A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))"
  then have reg:"∀T. T{is a topology}∧⋃T≈A ⟶ ((⋃T){is compact of cardinal} csucc(K){in}T)" using Spec_def by auto
  then have "A{is compact of cardinal} csucc(K) {in} Pow(A)" using Pow_is_top[of "A"] by auto
  then have "∀M∈Pow(Pow(A)). A⊆⋃M ⟶ (∃N∈Pow(M). A⊆⋃N ∧ N≺csucc(K))" unfolding IsCompactOfCard_def by auto
  moreover
  have "{{x}. x∈A}∈Pow(Pow(A))" by auto
  moreover
  have "A=⋃{{x}. x∈A}" by auto
  ultimately have "∃N∈Pow({{x}. x∈A}). A⊆⋃N ∧ N≺csucc(K)" by auto
  then obtain N where "N∈Pow({{x}. x∈A})" "A⊆⋃N" "N≺csucc(K)" by auto
  then have "N⊆{{x}. x∈A}" "N≺csucc(K)" "A⊆⋃N" using FinPow_def by auto
  {
    fix t
    assume "t∈{{x}. x∈A}"
    then obtain x where "x∈A""t={x}" by auto
    with ‹A⊆⋃N› have "x∈⋃N" by auto
    then obtain B where "B∈N""x∈B" by auto
    with ‹N⊆{{x}. x∈A}› have "B={x}" by auto
    with ‹t={x}›‹B∈N› have "t∈N" by auto 
  }
  with ‹N⊆{{x}. x∈A}› have "N={{x}. x∈A}" by auto
  let ?B="{⟨x,{x}⟩. x∈A}"
  from ‹N={{x}. x∈A}› have "?B:A→ N" unfolding Pi_def function_def by auto
  with ‹N={{x}. x∈A}› have "?B:inj(A,N)" unfolding inj_def using apply_equality by auto
  then have "A≲N" using lepoll_def by auto
  with ‹N≺csucc(K)› have "A≺csucc(K)" using lesspoll_trans1 by auto
  then show "A≲K" using Card_less_csucc_eq_le assms(2) by auto
next
  assume "A≲K"
  {
    fix T
    assume "T{is a topology}""⋃T≈A"
    have "Pow(⋃T){is a topology}" using Pow_is_top by auto
    {
      fix B
      assume AS:"B∈Pow(⋃T)"
      then have "{{i}. i∈B}⊆{{i} .i∈⋃T}" by auto
      moreover
      have "B=⋃{{i}. i∈B}" by auto
      ultimately have "∃S∈Pow({{i}. i∈⋃T}). B=⋃S" by auto
      then have "B∈{⋃U. U∈Pow({{i}. i∈⋃T})}" by auto
    }
    moreover
    {
      fix B
      assume AS:"B∈{⋃U. U∈Pow({{i}. i∈⋃T})}"
      then have "B∈Pow(⋃T)" by auto
    }
    ultimately
    have base:"{{x}. x∈⋃T} {is a base for}Pow(⋃T)" unfolding IsAbaseFor_def by auto
    let ?f="{⟨i,{i}⟩. i∈⋃T}"
    have f:"?f:⋃T→ {{x}. x∈⋃T}" using Pi_def function_def by auto
    moreover
    {
      fix w x
      assume as:"w∈⋃T""x∈⋃T""?f`w=?f`x"
      with f have "?f`w={w}" "?f`x={x}" using apply_equality by auto
      with as(3) have "w=x" by auto
    }
    with f have "?f:inj(⋃T,{{x}. x∈⋃T})" unfolding inj_def by auto
    moreover
    {
      fix xa
      assume "xa∈{{x}. x∈⋃T}"
      then obtain x where "x∈⋃T""xa={x}" by auto
      with f have "?f`x=xa" using apply_equality by auto
      with ‹x∈⋃T› have "∃x∈⋃T. ?f`x=xa" by auto
    }
    then have "∀xa∈{{x}. x∈⋃T}. ∃x∈⋃T. ?f`x=xa" by blast
    ultimately have "?f:bij(⋃T,{{x}. x∈⋃T})" unfolding bij_def surj_def by auto
    then have "⋃T≈{{x}. x∈⋃T}" using eqpoll_def by auto
    then have "{{x}. x∈⋃T}≈⋃T" using eqpoll_sym by auto
    with ‹⋃T≈A› have "{{x}. x∈⋃T}≈A" using eqpoll_trans by blast
    then have "{{x}. x∈⋃T}≲A" using eqpoll_imp_lepoll by auto
    with ‹A≲K› have "{{x}. x∈⋃T}≲K" using lepoll_trans by blast
    then have "{{x}. x∈⋃T}≺csucc(K)" using assms(2) Card_less_csucc_eq_le by auto
    with base have "Pow(⋃T) {is of second type of cardinal}csucc(K)" unfolding IsSecondOfCard_def by auto
    moreover
    have "⋃Pow(⋃T)=⋃T" by auto
    with calculation assms(1) ‹Pow(⋃T){is a topology}› have "(⋃T) {is compact of cardinal}csucc(K){in}Pow(⋃T)" 
      using compact_of_cardinal_Q[of "K""Pow(⋃T)"] by auto
    moreover
    have "T⊆Pow(⋃T)" by auto
    ultimately have "(⋃T) {is compact of cardinal}csucc(K){in}T" using compact_coarser by auto
  }
  then show "A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal}csucc(K) {in}T))" using Spec_def by auto
qed

theorem compactK_spectrum_reverse:
  assumes "∀A. (A {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))) ⟷ (A≲K)" "InfCard(K)"
  shows "{the axiom of}K{choice holds for subsets}(Pow(K))"
proof-
  have "K≲K" using lepoll_refl by auto
  then have "K {is in the spectrum of} (λT. ((⋃T){is compact of cardinal} csucc(K){in}T))" using assms(1) by auto
  moreover
  have "Pow(K){is a topology}" using Pow_is_top by auto
  moreover
  have "⋃Pow(K)=K" by auto
  then have "⋃Pow(K)≈K" using eqpoll_refl by auto
  ultimately
  have "K {is compact of cardinal} csucc(K){in}Pow(K)" using Spec_def by auto
  then show ?thesis using Q_disc_comp_csuccQ_eq_Q_choice_csuccQ assms(2) by auto
qed

text‹This last theorem states that if one of the forms of the axiom of choice related to this
compactness property fails, then the spectrum will be different. Notice that even for Lindelöf
spaces that will happend.›

text‹The spectrum gives us the posibility to define what an anti-property means.
A space is anti-‹P› if the only subspaces which have the property
are the ones in the spectrum of ‹P›. This concept tries to put together
spaces that are completely opposite to spaces where ‹P(T)›.›

definition
  antiProperty ("_{is anti-}_" 50)
  where "T{is anti-}P ≡ ∀A∈Pow(⋃T). P(T{restricted to}A) ⟶ (A {is in the spectrum of} P)"

abbreviation
  "ANTI(P) ≡ λT. (T{is anti-}P)"

text‹A first, very simple, but very useful result is the following: when the properties
are related and the spectra are equal, then the anti-properties are related in the oposite direction.›

theorem (in topology0) eq_spect_rev_imp_anti:
  assumes "∀T. T{is a topology} ⟶ P(T) ⟶ Q(T)" "∀A. (A{is in the spectrum of}Q) ⟶ (A{is in the spectrum of}P)"
    and "T{is anti-}Q"
  shows "T{is anti-}P"
proof-
  {
    fix A
    assume "A∈Pow(⋃T)""P(T{restricted to}A)"
    with assms(1) have "Q(T{restricted to}A)" using Top_1_L4 by auto
    with assms(3) ‹A∈Pow(⋃T)› have "A{is in the spectrum of}Q" using antiProperty_def by auto
    with assms(2) have "A{is in the spectrum of}P" by auto
  }
  then show ?thesis using antiProperty_def by auto
qed

text‹If a space can be ‹P(T)∧Q(T)› only in case the underlying set is in the
spectrum of ‹P›; then ‹Q(T)⟶ANTI(P,T)› when ‹Q› is hereditary.›

theorem Q_P_imp_Spec:
  assumes "∀T. ((T{is a topology}∧P(T)∧Q(T))⟶ ((⋃T){is in the spectrum of}P))"
    and "Q{is hereditary}"
  shows "∀T. T{is a topology} ⟶ (Q(T)⟶(T{is anti-}P))"
proof
  fix T
  {
    assume "T{is a topology}"
    {
      assume "Q(T)"
      {
        assume "¬(T{is anti-}P)"
        then obtain A where "A∈Pow(⋃T)" "P(T{restricted to}A)""¬(A{is in the spectrum of}P)"
          unfolding antiProperty_def by auto
        from ‹Q(T)›‹T{is a topology}›‹A∈Pow(⋃T)› assms(2) have "Q(T{restricted to}A)" 
          unfolding IsHer_def by auto
        moreover
        note ‹P(T{restricted to}A)› assms(1)
        moreover
        from ‹T{is a topology}› have "(T{restricted to}A){is a topology}" using topology0.Top_1_L4
          topology0_def by auto
        moreover
        from ‹A∈Pow(⋃T)› have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
        ultimately have "A{is in the spectrum of}P" by auto
        with ‹¬(A{is in the spectrum of}P)› have "False" by auto
      }
      then have "T{is anti-}P" by auto
    }
    then have "Q(T)⟶(T{is anti-}P)" by auto
  }
  then show "(T {is a topology}) ⟶ (Q(T) ⟶ (T{is anti-}P))" by auto
qed

text‹If a topologycal space has an hereditary property, then it has its double-anti property.›  

theorem (in topology0)her_P_imp_anti2P:
  assumes "P{is hereditary}" "P(T)"
  shows "T{is anti-}ANTI(P)"
proof-
  {
    assume "¬(T{is anti-}ANTI(P))"
    then have "∃A∈Pow(⋃T). ((T{restricted to}A){is anti-}P)∧¬(A{is in the spectrum of}ANTI(P))"
      unfolding antiProperty_def[of _ "ANTI(P)"] by auto
    then obtain A where A_def:"A∈Pow(⋃T)""¬(A{is in the spectrum of}ANTI(P))""(T{restricted to}A){is anti-}P"
      by auto
    from ‹A∈Pow(⋃T)› have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
    from A_def have reg:"∀B∈Pow(⋃(T{restricted to}A)). P((T{restricted to}A){restricted to}B) ⟶ (B{is in the spectrum of}P)"
      unfolding antiProperty_def by auto
    have "∀B∈Pow(A). (T{restricted to}A){restricted to}B=T{restricted to}B" using subspace_of_subspace ‹A∈Pow(⋃T)› by auto
    then have "∀B∈Pow(A). P(T{restricted to}B) ⟶ (B{is in the spectrum of}P)" using reg tot
      by force
    moreover
    have "∀B∈Pow(A). P(T{restricted to}B)" using assms ‹A∈Pow(⋃T)› unfolding IsHer_def using topSpaceAssum by blast
    ultimately have reg2:"∀B∈Pow(A). (B{is in the spectrum of}P)" by auto
    from ‹¬(A{is in the spectrum of}ANTI(P))› have "∃T. T{is a topology} ∧ ⋃T≈A ∧ ¬(T{is anti-}P)"
      unfolding Spec_def by auto
    then obtain S where "S{is a topology}" "⋃S≈A" "¬(S{is anti-}P)" by auto
    from ‹¬(S{is anti-}P)› have "∃B∈Pow(⋃S). P(S{restricted to}B) ∧ ¬(B{is in the spectrum of}P)" unfolding antiProperty_def by auto
    then obtain B where B_def:"¬(B{is in the spectrum of}P)" "B∈Pow(⋃S)" by auto
    then have "B≲⋃S" using subset_imp_lepoll by auto
    with ‹⋃S≈A› have "B≲A" using lepoll_eq_trans by auto
    then obtain f where "f∈inj(B,A)" unfolding lepoll_def by auto
    then have "f∈bij(B,range(f))" using inj_bij_range by auto
    then have "B≈range(f)" unfolding eqpoll_def by auto
    with B_def(1) have "¬(range(f){is in the spectrum of}P)" using eqpoll_iff_spec by auto
    moreover
    with ‹f∈inj(B,A)› have "range(f)⊆A" unfolding inj_def Pi_def by auto
    with reg2 have "range(f){is in the spectrum of}P" by auto
    ultimately have "False" by auto
  }
  then show ?thesis by auto
qed
  
text‹The anti-properties are always hereditary›

theorem anti_here:
  shows "ANTI(P){is hereditary}"
proof-
  {
    fix T
    assume "T {is a topology}""ANTI(P,T)"
    {
      fix A
      assume "A∈Pow(⋃T)"
      then have "⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
      moreover
      {
        fix B
        assume "B∈Pow(A)""P((T{restricted to}A){restricted to}B)"
        with ‹A∈Pow(⋃T)› have "B∈Pow(⋃T)""P(T{restricted to}B)" using subspace_of_subspace by auto
        with ‹ANTI(P,T)› have "B{is in the spectrum of}P" unfolding antiProperty_def by auto
      }
      ultimately have "∀B∈Pow(⋃(T{restricted to}A)). (P((T{restricted to}A){restricted to}B)) ⟶ (B{is in the spectrum of}P)"
        by auto
      then have "ANTI(P,(T{restricted to}A))" unfolding antiProperty_def by auto
    }
    then have "∀A∈Pow(⋃T). ANTI(P,(T{restricted to}A))" by auto
  }
  then show ?thesis using IsHer_def by auto
qed

corollary (in topology0) anti_imp_anti3:
  assumes "T{is anti-}P"
  shows "T{is anti-}ANTI(ANTI(P))"
  using anti_here her_P_imp_anti2P assms by auto

text‹In the article \cite{ReVa80}, we can find some results on anti-properties.›

theorem (in topology0) anti_T0:
  shows "(T{is anti-}isT0) ⟷ T={0,⋃T}"
proof
  assume "T={0,⋃T}"
  {
    fix A
    assume "A∈Pow(⋃T)""(T{restricted to}A) {is T⇩0}"
    {
      fix B
      assume "B∈T{restricted to}A"
      then obtain S where "S∈T" and "B=A∩S" unfolding RestrictedTo_def by auto
      with ‹T={0,⋃T}› have "S∈{0,⋃T}" by auto
      then have "S=0∨S=⋃T" by auto
      with ‹B=A∩S›‹A∈Pow(⋃T)› have "B=0∨B=A" by auto
    }
    moreover
    {
      have "0∈{0,⋃T}" "⋃T∈{0,⋃T}" by auto
      with ‹T={0,⋃T}› have "0∈T""(⋃T)∈T" by auto
      then have "A∩0∈(T{restricted to}A)" "A∩(⋃T)∈(T{restricted to}A)" using RestrictedTo_def by auto
      moreover
      from ‹A∈Pow(⋃T)› have "A∩(⋃T)=A" by auto
      ultimately have "0∈(T{restricted to}A)" "A∈(T{restricted to}A)" by auto
    }
    ultimately have "(T{restricted to}A)={0,A}" by auto
    with ‹(T{restricted to}A) {is T⇩0}› have "{0,A} {is T⇩0}" by auto
    {
      assume "A≠0"
      then obtain x where "x∈A" by blast
      {
        fix y
        assume "y∈A""x≠y"
        with ‹{0,A} {is T⇩0}› obtain U where "U∈{0,A}" and dis:"(x ∈ U ∧ y ∉ U) ∨ (y ∈ U ∧ x ∉ U)" using isT0_def by auto
        then have "U=A" by auto
        with dis ‹y∈A› ‹x∈A› have "False" by auto
      }
      then have "∀y∈A. y=x" by auto
      with ‹x∈A› have "A={x}" by blast
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
      then have "A{is in the spectrum of}isT0" using T0_spectrum by auto   
    }
    moreover
    {
      assume "A=0"
      then have "A≈0" by auto
      then have "A≲1" using empty_lepollI eq_lepoll_trans by auto
      then have "A{is in the spectrum of}isT0" using T0_spectrum by auto
    }
    ultimately have "A{is in the spectrum of}isT0" by auto
  }
  then show "T{is anti-}isT0" using antiProperty_def by auto
next
  assume "T{is anti-}isT0"
  then have "∀A∈Pow(⋃T). (T{restricted to}A){is T⇩0} ⟶ (A{is in the spectrum of}isT0)" using antiProperty_def by auto
  then have reg:"∀A∈Pow(⋃T). (T{restricted to}A){is T⇩0} ⟶ (A≲1)" using T0_spectrum by auto
  {
    assume "∃A∈T. A≠0∧ A≠⋃T"
    then obtain A where "A∈T""A≠0""A≠⋃T" by auto
    then obtain x y where "x∈A" "y∈⋃T-A" by blast
    with ‹A∈T› have s:"{x,y}∈Pow(⋃T)" "x≠y" by auto
    note s
    moreover
    {
      fix b1 b2
      assume "b1∈⋃(T{restricted to}{x,y})""b2∈⋃(T{restricted to}{x,y})""b1≠b2"
      moreover
      from s have "⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto
      ultimately have "(b1=x∧b2=y)∨(b1=y∧b2=x)" by auto
      with ‹x≠y› have "(b1∈{x}∧b2∉{x}) ∨ (b2∈{x}∧b1∉{x})" by auto
      moreover
      from ‹y∈⋃T-A›‹x∈A› have "{x}={x,y}∩A" by auto
      with ‹A∈T› have "{x}∈(T{restricted to}{x,y})" unfolding RestrictedTo_def by auto
      ultimately have "∃U∈(T{restricted to}{x,y}). (b1∈U∧b2∉U) ∨ (b2∈U∧b1∉U)" by auto
    }
    then have "(T{restricted to}{x,y}){is T⇩0}" using isT0_def by auto
    ultimately have "{x,y}≲1" using reg by auto
    moreover
    have "x∈{x,y}" by auto
    ultimately have "{x,y}={x}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
    moreover
    have "y∈{x,y}" by auto
    ultimately have "y∈{x}" by auto
    then have "y=x" by auto
    with ‹x≠y› have "False" by auto
  }
  then have "T⊆{0,⋃T}" by auto
  moreover
  from topSpaceAssum have "0∈T""⋃T∈T" using IsATopology_def empty_open by auto
  ultimately show "T={0,⋃T}" by auto
qed

lemma indiscrete_spectrum:
  shows "(A {is in the spectrum of}(λT. T={0,⋃T})) ⟷ A≲1"
proof
  assume "(A {is in the spectrum of}(λT. T={0,⋃T}))"
  then have reg:"∀T. ((T{is a topology} ∧ ⋃T≈A) ⟶ T ={0,⋃T})" using Spec_def by auto
  moreover
  have "⋃Pow(A)=A" by auto
  then have "⋃Pow(A)≈A" by auto
  moreover
  have "Pow(A) {is a topology}" using Pow_is_top by auto
  ultimately have P:"Pow(A)={0,A}" by auto
  {
    assume "A≠0"
    then obtain x where "x∈A" by blast
    then have "{x}∈Pow(A)" by auto
    with P have "{x}=A" 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 show "A≲1" by auto
next
  assume "A≲1"
  {
    fix T
    assume "T{is a topology}""⋃T≈A"
    {
      assume "A=0"
      with ‹⋃T≈A› have "⋃T≈0" by auto
      then have "⋃T=0" using eqpoll_0_is_0 by auto
      then have "T⊆{0}" by auto
      with ‹T{is a topology}› have "T={0}" using empty_open by auto
      then have "T={0,⋃T}" by auto
    }
    moreover
    {
      assume "A≠0"
      then obtain E where "E∈A" by blast
      with ‹A≲1› have "A={E}" using lepoll_1_is_sing by auto
      then have "A≈1" using singleton_eqpoll_1 by auto
      with ‹⋃T≈A› have NONempty:"⋃T≈1" using eqpoll_trans by blast
      then have "⋃T≲1" using eqpoll_imp_lepoll by auto
      moreover
      {
        assume "⋃T=0"
        then have "0≈⋃T" by auto
        with NONempty have "0≈1" using eqpoll_trans by blast
        then have "0=1" using eqpoll_0_is_0 eqpoll_sym by auto
        then have "False" by auto
      }
      then have "⋃T≠0" by auto
      then obtain R where "R∈⋃T" by blast
      ultimately have "⋃T={R}" using lepoll_1_is_sing by auto
      moreover
      have "T⊆Pow(⋃T)" by auto
      ultimately have "T⊆Pow({R})" by auto
      then have "T⊆{0,{R}}" by blast
      moreover
      with ‹T{is a topology}› have "0∈T""⋃T∈T" using IsATopology_def by auto
      moreover
      note ‹⋃T={R}›
      ultimately have "T={0,⋃T}" by auto
    }
    ultimately have "T={0,⋃T}" by auto
  }
  then show "A {is in the spectrum of}(λT. T={0,⋃T})" using Spec_def by auto
qed

theorem (in topology0) anti_indiscrete:
  shows "(T{is anti-}(λT. T={0,⋃T})) ⟷ T{is T⇩0}"
proof
  assume "T{is T⇩0}"
  {
    fix A
    assume "A∈Pow(⋃T)""T{restricted to}A={0,⋃(T{restricted to}A)}"
    then have un:"⋃(T{restricted to}A)=A" "T{restricted to}A={0,A}" using RestrictedTo_def by auto
    from ‹T{is T⇩0}›‹A∈Pow(⋃T)› have "(T{restricted to}A){is T⇩0}" using T0_here by auto
    {
      assume "A=0"
      then have "A≈0" by auto
      then have "A≲1" using empty_lepollI eq_lepoll_trans by auto
    }
    moreover
    {
      assume "A≠0"
      then obtain E where "E∈A" by blast
      {
        fix y
        assume "y∈A""y≠E"
        with ‹E∈A› un have "y∈⋃(T{restricted to}A)""E∈⋃(T{restricted to}A)" by auto
        with ‹(T{restricted to}A){is T⇩0}›‹y≠E› have "∃U∈(T{restricted to}A). (E∈U∧y∉U)∨(E∉U∧y∈U)"
          unfolding isT0_def by blast
        then obtain U where "U∈(T{restricted to}A)" "(E∈U∧y∉U)∨(E∉U∧y∈U)" by auto
        with ‹T{restricted to}A={0,A}› have "U=0∨U=A" by auto
        with ‹(E∈U∧y∉U)∨(E∉U∧y∈U)›‹y∈A›‹E∈A› have "False" by auto
      }
      then have "∀y∈A. y=E" by auto
      with ‹E∈A› have "A={E}" by blast
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
    }
    ultimately have "A≲1" by auto
    then have "A{is in the spectrum of}(λT. T={0,⋃T})" using indiscrete_spectrum by auto
  }
  then show "T{is anti-}(λT. T={0,⋃T})" unfolding antiProperty_def by auto
next
  assume "T{is anti-}(λT. T={0,⋃T})"
  then have "∀A∈Pow(⋃T). (T{restricted to}A)={0,⋃(T{restricted to}A)} ⟶ (A {is in the spectrum of} (λT. T={0,⋃T}))" using antiProperty_def by auto
  then have "∀A∈Pow(⋃T). (T{restricted to}A)={0,⋃(T{restricted to}A)} ⟶ A≲1" using indiscrete_spectrum by auto
  moreover
  have "∀A∈Pow(⋃T). ⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
  ultimately have reg:"∀A∈Pow(⋃T). (T{restricted to}A)={0,A} ⟶ A≲1" by auto
  {
    fix x y
    assume "x∈⋃T""y∈⋃T""x≠y"
    {
      assume "∀U∈T. (x∈U∧y∈U)∨(x∉U∧y∉U)"
      then have "T{restricted to}{x,y}⊆{0,{x,y}}" unfolding RestrictedTo_def by auto
      moreover
      from ‹x∈⋃T›‹y∈⋃T› have emp:"0∈T""{x,y}∩0=0" and tot: "{x,y}={x,y}∩⋃T" "⋃T∈T" using topSpaceAssum empty_open IsATopology_def by auto
      from emp have "0∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto
      moreover
      from tot have "{x,y}∈T{restricted to}{x,y}" unfolding RestrictedTo_def by auto
      ultimately have "T{restricted to}{x,y}={0,{x,y}}" by auto
      with reg ‹x∈⋃T›‹y∈⋃T› have "{x,y}≲1" by auto
      moreover
      have "x∈{x,y}" by auto
      ultimately have "{x,y}={x}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
      moreover
      have "y∈{x,y}" by auto
      ultimately have "y∈{x}" by auto
      then have "y=x" by auto
      then have "False" using ‹x≠y› by auto
    }
    then have "∃U∈T. (x∉U∨y∉U)∧(x∈U∨y∈U)" by auto
    then have "∃U∈T. (x∈U∧y∉U)∨(x∉U∧y∈U)" by auto
  }
  then have "∀x y. x∈⋃T∧y∈⋃T∧ x≠y ⟶ (∃U∈T. (x∈U∧y∉U)∨(y∈U∧x∉U))" by auto
  then show "T {is T⇩0}" using isT0_def by auto
qed

text‹The conclusion is that being $T_0$ is just the opposite to being indiscrete.›

text‹Next, let's compute the anti-$T_i$ for $i=1,\ 2,\ 3$ or $4$. Surprisingly, 
they are all the same. Meaning, that the total negation of $T_1$ is enough
to negate all of these axioms.›

theorem anti_T1:
  shows "(T{is anti-}isT1) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
proof
  assume "T{is anti-}isT1"
  let ?r="{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}"
  have "antisym(?r)" unfolding antisym_def by auto
  moreover
  have "trans(?r)" unfolding trans_def by auto
  moreover
  {
    fix A B
    assume "A∈T""B∈T"
    {
      assume "¬(A⊆B∨B⊆A)"
      then have "A-B≠0""B-A≠0" by auto
      then obtain x y where "x∈A""x∉B""y∈B""y∉A" "x≠y" by blast
      then have "{x,y}∩A={x}""{x,y}∩B={y}" by auto
      moreover
      from ‹A∈T›‹B∈T› have "{x,y}∩A∈T{restricted to}{x,y}""{x,y}∩B∈T{restricted to}{x,y}" unfolding
        RestrictedTo_def by auto
      ultimately have open_set:"{x}∈T{restricted to}{x,y}""{y}∈T{restricted to}{x,y}" by auto
      have "x∈⋃T""y∈⋃T" using ‹A∈T›‹B∈T›‹x∈A›‹y∈B› by auto
      then have sub:"{x,y}∈Pow(⋃T)" by auto
      then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto
      {
        fix s t
        assume "s∈⋃(T{restricted to}{x,y})""t∈⋃(T{restricted to}{x,y})""s≠t"
        with tot have "s∈{x,y}""t∈{x,y}""s≠t" by auto
        then have "(s=x∧t=y)∨(s=y∧t=x)" by auto
        with open_set have "∃U∈(T{restricted to}{x,y}). s∈U∧t∉U" using ‹x≠y› by auto
      }
      then have "(T{restricted to}{x,y}){is T⇩1}" unfolding isT1_def by auto
      with sub ‹T{is anti-}isT1› tot have "{x,y} {is in the spectrum of}isT1" using antiProperty_def
        by auto
      then have "{x,y}≲1" using T1_spectrum by auto
      moreover
      have "x∈{x,y}" by auto
      ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
      moreover
      have "y∈{x,y}" by auto
      ultimately
      have "y∈{x}" by auto
      then have "x=y" by auto
      then have "False" using ‹x∈A›‹y∉A› by auto
    }
    then have "A⊆B∨B⊆A" by auto
  }
  then have "?r {is total on}T" using IsTotal_def by auto
  ultimately
  show "IsLinOrder(T,?r)" using IsLinOrder_def by auto
next
  assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"
  then have ordTot:"∀S∈T. ∀B∈T. S⊆B∨B⊆S" unfolding IsLinOrder_def IsTotal_def by auto
  {
    fix A
    assume "A∈Pow(⋃T)" and T1:"(T{restricted to}A) {is T⇩1}"
    then have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def by auto
    {
      fix U V
      assume "U∈T{restricted to}A""V∈T{restricted to}A"
      then obtain AU AV where "AU∈T""AV∈T""U=A∩AU""V=A∩AV" unfolding RestrictedTo_def by auto
      with ordTot have "U⊆V∨V⊆U" by auto
    }
    then have ordTotSub:"∀S∈T{restricted to}A. ∀B∈T{restricted to}A. S⊆B∨B⊆S" by auto
    {
      assume "A=0"
      then have "A≈0" by auto
      moreover
      have "0≲1" using empty_lepollI by auto
      ultimately have "A≲1" using eq_lepoll_trans by auto
      then have "A{is in the spectrum of}isT1" using T1_spectrum by auto
    }
    moreover
    {
      assume "A≠0"
      then obtain t where "t∈A" by blast
      {
        fix y
        assume "y∈A""y≠t"
        with ‹t∈A› tot T1 obtain U where "U∈(T{restricted to}A)""y∈U""t∉U" unfolding isT1_def
          by auto
        from ‹y≠t› have "t≠y" by auto
        with ‹y∈A›‹t∈A› tot T1 obtain V where "V∈(T{restricted to}A)""t∈V""y∉V" unfolding isT1_def
          by auto
        with ‹y∈U›‹t∉U› have "¬(U⊆V∨V⊆U)" by auto
        with ordTotSub ‹U∈(T{restricted to}A)›‹V∈(T{restricted to}A)› have "False" by auto
      }
      then have "∀y∈A. y=t" by auto
      with ‹t∈A› have "A={t}" by blast
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
      then have "A{is in the spectrum of}isT1" using T1_spectrum by auto
    }
    ultimately
    have "A{is in the spectrum of}isT1" by auto
  }
  then show "T{is anti-}isT1" using antiProperty_def by auto
qed

corollary linordtop_here:
  shows "(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})){is hereditary}"
  using anti_T1 anti_here[of "isT1"] by auto

theorem (in topology0) anti_T4:
  shows "(T{is anti-}isT4) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
proof
  assume "T{is anti-}isT4"
  let ?r="{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}"
  have "antisym(?r)" unfolding antisym_def by auto
  moreover
  have "trans(?r)" unfolding trans_def by auto
  moreover
  {
    fix A B
    assume "A∈T""B∈T"
    {
      assume "¬(A⊆B∨B⊆A)"
      then have "A-B≠0""B-A≠0" by auto
      then obtain x y where "x∈A""x∉B""y∈B""y∉A" "x≠y" by blast
      then have "{x,y}∩A={x}""{x,y}∩B={y}" by auto
      moreover
      from ‹A∈T›‹B∈T› have "{x,y}∩A∈T{restricted to}{x,y}""{x,y}∩B∈T{restricted to}{x,y}" unfolding
        RestrictedTo_def by auto
      ultimately have open_set:"{x}∈T{restricted to}{x,y}""{y}∈T{restricted to}{x,y}" by auto
      have "x∈⋃T""y∈⋃T" using ‹A∈T›‹B∈T›‹x∈A›‹y∈B› by auto
      then have sub:"{x,y}∈Pow(⋃T)" by auto
      then have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def by auto
      {
        fix s t
        assume "s∈⋃(T{restricted to}{x,y})""t∈⋃(T{restricted to}{x,y})""s≠t"
        with tot have "s∈{x,y}""t∈{x,y}""s≠t" by auto
        then have "(s=x∧t=y)∨(s=y∧t=x)" by auto
        with open_set have "∃U∈(T{restricted to}{x,y}). s∈U∧t∉U" using ‹x≠y› by auto
      }
      then have "(T{restricted to}{x,y}){is T⇩1}" unfolding isT1_def by auto
      moreover
      {
        fix s
        assume AS:"s{is closed in}(T{restricted to}{x,y})"
        {
          fix t
          assume AS2:"t{is closed in}(T{restricted to}{x,y})""s∩t=0"
          have "(T{restricted to}{x,y}){is a topology}" using Top_1_L4 by auto
          with tot have "0∈(T{restricted to}{x,y})""{x,y}∈(T{restricted to}{x,y})" using empty_open
            union_open[where 𝒜="T{restricted to}{x,y}"] by auto
          moreover
          note open_set
          moreover
          have "T{restricted to}{x,y}⊆Pow(⋃(T{restricted to}{x,y}))" by blast
          with tot have "T{restricted to}{x,y}⊆Pow({x,y})" by auto
          ultimately have "T{restricted to}{x,y}={0,{x},{y},{x,y}}" by blast
          moreover have "{0,{x},{y},{x,y}}=Pow({x,y})" by blast
          ultimately have P:"T{restricted to}{x,y}=Pow({x,y})" by simp
          with tot have "{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}={A ∈ Pow({x, y}) . A ⊆ {x, y} ∧ {x, y} - A ∈ Pow({x, y})}" using IsClosed_def by simp
          with P have S:"{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}=T{restricted to}{x,y}" by auto
          from AS AS2(1) have "s∈Pow({x,y})" "t∈Pow({x,y})" using IsClosed_def tot by auto
          moreover
          note AS2(1) AS
          ultimately have "s∈{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}""t∈{A∈Pow({x,y}). A{is closed in}(T{restricted to}{x,y})}"
            by auto
          with S AS2(2) have "s∈T{restricted to}{x,y}" "t∈T{restricted to}{x,y}""s∩t=0" by auto
          then have "∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0" by auto
        }
        then have "∀t. t{is closed in}(T{restricted to}{x,y})∧s∩t=0 ⟶ (∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0)"
          by auto
      }
      then have "∀s. s{is closed in}(T{restricted to}{x,y}) ⟶ (∀t. t{is closed in}(T{restricted to}{x,y})∧s∩t=0 ⟶ (∃U∈(T{restricted to}{x,y}). ∃V∈(T{restricted to}{x,y}). s⊆U∧t⊆V∧U∩V=0))"
        by auto
      then have "(T{restricted to}{x,y}){is normal}" using IsNormal_def by auto
      ultimately have "(T{restricted to}{x,y}){is T⇩4}" using isT4_def by auto
      with sub ‹T{is anti-}isT4› tot have "{x,y} {is in the spectrum of}isT4" using antiProperty_def
        by auto
      then have "{x,y}≲1" using T4_spectrum by auto
      moreover
      have "x∈{x,y}" by auto
      ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
      moreover
      have "y∈{x,y}" by auto
      ultimately
      have "y∈{x}" by auto
      then have "x=y" by auto
      then have "False" using ‹x∈A›‹y∉A› by auto
    }
    then have "A⊆B∨B⊆A" by auto
  }
  then have "?r {is total on}T" using IsTotal_def by auto
  ultimately
  show "IsLinOrder(T,?r)" using IsLinOrder_def by auto
next
  assume "IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V})"
  then have "T{is anti-}isT1" using anti_T1 by auto
  moreover
  have "∀T. T{is a topology} ⟶ (T{is T⇩4}) ⟶ (T{is T⇩1})" using topology0.T4_is_T3 
    topology0.T3_is_T2 T2_is_T1 topology0_def by auto
  moreover
  have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT4)" using T1_spectrum T4_spectrum
    by auto
  ultimately show "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT1"] by auto
qed

theorem (in topology0) anti_T3:
  shows "(T{is anti-}isT3) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
proof
  assume "T{is anti-}isT3"
  moreover
  have "∀T. T{is a topology} ⟶ (T{is T⇩4}) ⟶ (T{is T⇩3})" using topology0.T4_is_T3 
    topology0_def by auto
  moreover
  have " ∀A. (A {is in the spectrum of} isT3) ⟶ (A {is in the spectrum of} isT4)" using T3_spectrum T4_spectrum
    by auto
  ultimately have "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT3"] by auto
  then show "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" using anti_T4 by auto
next
  assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"
  then have "T{is anti-}isT1" using anti_T1 by auto
  moreover
  have "∀T. T{is a topology} ⟶ (T{is T⇩3}) ⟶ (T{is T⇩1})" using
    topology0.T3_is_T2 T2_is_T1 topology0_def by auto
  moreover
  have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT3)" using T1_spectrum T3_spectrum
    by auto
  ultimately show "T{is anti-}isT3" using eq_spect_rev_imp_anti[of "isT3""isT1"] by auto
qed

theorem (in topology0) anti_T2:
  shows "(T{is anti-}isT2) ⟷ (IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
proof
  assume "T{is anti-}isT2"
  moreover
  have "∀T. T{is a topology} ⟶ (T{is T⇩4}) ⟶ (T{is T⇩2})" using topology0.T4_is_T3 
    topology0.T3_is_T2 topology0_def by auto
  moreover
  have " ∀A. (A {is in the spectrum of} isT2) ⟶ (A {is in the spectrum of} isT4)" using T2_spectrum T4_spectrum
    by auto
  ultimately have "T{is anti-}isT4" using eq_spect_rev_imp_anti[of "isT4""isT2"] by auto
  then show "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" using anti_T4 by auto
next
  assume "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"
  then have "T{is anti-}isT1" using anti_T1 by auto
  moreover
  have "∀T. T{is a topology} ⟶ (T{is T⇩2}) ⟶ (T{is T⇩1})" using T2_is_T1 by auto
  moreover
  have " ∀A. (A {is in the spectrum of} isT1) ⟶ (A {is in the spectrum of} isT2)" using T1_spectrum T2_spectrum
    by auto
  ultimately show "T{is anti-}isT2" using eq_spect_rev_imp_anti[of "isT2""isT1"] by auto
qed

lemma linord_spectrum:
  shows "(A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))) ⟷ A≲1"
proof
  assume "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
  then have reg:"∀T. T{is a topology}∧ ⋃T≈A ⟶ IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"
    using Spec_def by auto
  {
    assume "A=0"
    moreover
    have "0≲1" using empty_lepollI by auto
    ultimately have "A≲1" using eq_lepoll_trans by auto
  }
  moreover
  { 
    assume "A≠0"
    then obtain x where "x∈A" by blast
    moreover
    {
      fix y
      assume "y∈A"
      have "Pow(A) {is a topology}" using Pow_is_top by auto
      moreover
      have "⋃Pow(A)=A" by auto
      then have "⋃Pow(A)≈A" by auto
      note reg
      ultimately have "IsLinOrder(Pow(A),{⟨U,V⟩∈Pow(⋃Pow(A))×Pow(⋃Pow(A)). U⊆V})" by auto
      then have "IsLinOrder(Pow(A),{⟨U,V⟩∈Pow(A)×Pow(A). U⊆V})" by auto
      with ‹x∈A›‹y∈A› have "{x}⊆{y}∨{y}⊆{x}" unfolding IsLinOrder_def IsTotal_def by auto
      then have "x=y" by auto
    }
    ultimately have "A={x}" by blast
    then have "A≈1" using singleton_eqpoll_1 by auto
    then have "A≲1" using eqpoll_imp_lepoll by auto
  }
  ultimately show "A≲1" by auto
next
  assume "A≲1"
  then have ind:"A{is in the spectrum of}(λT. T={0,⋃T})" using indiscrete_spectrum by auto
  {
    fix T
    assume AS:"T{is a topology}" "T={0,⋃T}"
    have "trans({⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding trans_def by auto
    moreover
    have "antisym({⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding antisym_def by auto
    moreover
    have "{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}{is total on}T"
    proof-
      {
        fix aa b
        assume "aa∈T""b∈T"
        with AS(2) have "aa∈{0,⋃T}""b∈{0,⋃T}" by auto
        then have "aa=0∨aa=⋃T""b=0∨b=⋃T" by auto
        then have "aa⊆b∨b⊆aa" by auto
        then have "⟨aa, b⟩ ∈ Collect(Pow(⋃T) × Pow(⋃T), split((⊆))) ∨ ⟨b, aa⟩ ∈ Collect(Pow(⋃T) × Pow(⋃T), split((⊆)))"
        using ‹aa∈T›‹b∈T› by auto
      }
      then show ?thesis using IsTotal_def by auto
    qed
    ultimately have "IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})" unfolding IsLinOrder_def by auto
  }
  then have " ∀T. T {is a topology} ⟶ T = {0, ⋃T} ⟶ IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V})" by auto
  then show "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
    using P_imp_Q_spec_inv[of "λT. T={0,⋃T}""λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V})"]
    ind by auto
qed

theorem (in topology0) anti_linord:
  shows "(T{is anti-}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))) ⟷ T{is T⇩1}"
proof
  assume AS:"T{is anti-}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))"
  {
    assume "¬(T{is T⇩1})"
    then obtain x y where "x∈⋃T""y∈⋃T""x≠y""∀U∈T. x∉U∨y∈U" unfolding isT1_def by auto
    {
      assume "{x}∈T{restricted to}{x,y}"
      then obtain U where "U∈T" "{x}={x,y}∩U" unfolding RestrictedTo_def by auto
      moreover
      have "x∈{x}" by auto
      ultimately have "U∈T""x∈U" by auto
      moreover
      {
        assume "y∈U"
        then have "y∈{x,y}∩U" by auto
        with ‹{x}={x,y}∩U› have "y∈{x}" by auto
        with ‹x≠y› have "False" by auto
      }
      then have "y∉U" by auto
      moreover
      note ‹∀U∈T. x∉U∨y∈U›
      ultimately have "False" by auto
    }
    then have "{x}∉T{restricted to}{x,y}" by auto
    moreover
    have tot:"⋃(T{restricted to}{x,y})={x,y}" using ‹x∈⋃T›‹y∈⋃T› unfolding RestrictedTo_def by auto
    moreover
    have "T{restricted to}{x,y}⊆Pow(⋃(T{restricted to}{x,y}))" by auto
    ultimately have "T{restricted to}{x,y}⊆Pow({x,y})-{{x}}" by auto
    moreover
    have "Pow({x,y})={0,{x,y},{x},{y}}" by blast
    ultimately have "T{restricted to}{x,y}⊆{0,{x,y},{y}}" by auto
    moreover
    have "IsLinOrder({0,{x,y},{y}},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})"
    proof-
      have "antisym(Collect(Pow({x, y}) × Pow({x, y}), split((⊆))))" using antisym_def by auto
      moreover
      have "trans(Collect(Pow({x, y}) × Pow({x, y}), split((⊆))))" using trans_def by auto
      moreover
      have "Collect(Pow({x, y}) × Pow({x, y}), split((⊆))) {is total on} {0, {x, y}, {y}}" using IsTotal_def by auto
      ultimately show "IsLinOrder({0,{x,y},{y}},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" using IsLinOrder_def by auto
    qed
    ultimately have "IsLinOrder(T{restricted to}{x,y},{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" using ord_linear_subset
      by auto
    with tot have "IsLinOrder(T{restricted to}{x,y},{⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V})"
      by auto
    then have "IsLinOrder(T{restricted to}{x,y},Collect(Pow(⋃(T {restricted to} {x,y})) × Pow(⋃(T {restricted to} {x,y})), split((⊆))))" by auto
    moreover
    from ‹x∈⋃T›‹y∈⋃T› have "{x,y}∈Pow(⋃T)" by auto
    moreover
    note AS
    ultimately have "{x,y}{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" unfolding antiProperty_def
      by simp
    then have "{x,y}≲1" using linord_spectrum by auto
    moreover
    have "x∈{x,y}" by auto
    ultimately have "{x}={x,y}" using lepoll_1_is_sing[of "{x,y}""x"] by auto
    moreover
    have "y∈{x,y}" by auto
    ultimately
    have "y∈{x}" by auto
    then have "x=y" by auto
    then have "False" using ‹x≠y› by auto
  }
  then show "T {is T⇩1}" by auto
next
  assume T1:"T {is T⇩1}"
  {
    fix A
    assume A_def:"A∈Pow(⋃T)""IsLinOrder((T{restricted to}A) ,{⟨U,V⟩∈Pow(⋃(T{restricted to}A))×Pow(⋃(T{restricted to}A)). U⊆V})"
    {
      fix x 
      assume AS1:"x∈A"
      {
        fix y
        assume AS:"y∈A""x≠y"
        with AS1 have "{x,y}∈Pow(⋃T)" using ‹A∈Pow(⋃T)› by auto
        from ‹x∈A›‹y∈A› have "{x,y}∈Pow(A)" by auto
        from ‹{x,y}∈Pow(⋃T)› have T11:"(T{restricted to}{x,y}){is T⇩1}" using T1_here T1 by auto
        moreover
        have tot:"⋃(T{restricted to}{x,y})={x,y}" unfolding RestrictedTo_def using ‹{x,y}∈Pow(⋃T)› by auto
        moreover
        note AS(2) 
        ultimately obtain U where "x∈U""y∉U""U∈(T{restricted to}{x,y})" unfolding isT1_def by auto
        moreover
        from AS(2) tot T11 obtain V where "y∈V""x∉V""V∈(T{restricted to}{x,y})" unfolding isT1_def by auto
        ultimately have "x∈U-V""y∈V-U""U∈(T{restricted to}{x,y})""V∈(T{restricted to}{x,y})" by auto
        then have "¬(U⊆V∨V⊆U)""U∈(T{restricted to}{x,y})""V∈(T{restricted to}{x,y})" by auto
        then have "¬({⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V} {is total on} (T{restricted to}{x,y}))"
          unfolding IsTotal_def by auto
        then have "¬(IsLinOrder((T{restricted to}{x,y}),{⟨U,V⟩∈Pow(⋃(T{restricted to}{x,y}))×Pow(⋃(T{restricted to}{x,y})). U⊆V}))"
          unfolding IsLinOrder_def by auto
        moreover
        {
          have "(T{restricted to}A) {is a topology}" using Top_1_L4 by auto
          moreover
          note A_def(2) linordtop_here
          ultimately have "∀B∈Pow(⋃(T{restricted to}A)). IsLinOrder((T{restricted to}A){restricted to}B ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})"
            unfolding IsHer_def by auto
          moreover
          have tot:"⋃(T{restricted to}A)=A" unfolding RestrictedTo_def using ‹A∈Pow(⋃T)› by auto
          ultimately have  "∀B∈Pow(A). IsLinOrder((T{restricted to}A){restricted to}B ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})" by auto
          moreover
          have "∀B∈Pow(A). (T{restricted to}A){restricted to}B=T{restricted to}B" using subspace_of_subspace ‹A∈Pow(⋃T)› by auto
          ultimately
          have "∀B∈Pow(A). IsLinOrder((T{restricted to}B) ,{⟨U,V⟩∈Pow(⋃((T{restricted to}A){restricted to}B))×Pow(⋃((T{restricted to}A){restricted to}B)). U⊆V})" by auto
          moreover
          have "∀B∈Pow(A). ⋃((T{restricted to}A){restricted to}B)=B" using ‹A∈Pow(⋃T)› unfolding RestrictedTo_def by auto
          ultimately have "∀B∈Pow(A). IsLinOrder((T{restricted to}B) ,{⟨U,V⟩∈Pow(B)×Pow(B). U⊆V})" by auto
          with ‹{x,y}∈Pow(A)› have "IsLinOrder((T{restricted to}{x,y}) ,{⟨U,V⟩∈Pow({x,y})×Pow({x,y}). U⊆V})" by auto
        }
        ultimately have "False" using tot by auto
      }
      then have "A={x}" using AS1 by auto
      then have "A≈1" using singleton_eqpoll_1 by auto
      then have "A≲1" using eqpoll_imp_lepoll by auto
      then have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" using linord_spectrum
        by auto
    }
    moreover
    {
      assume "A=0"
      then have "A≈0" by auto
      moreover
      have "0≲1" using empty_lepollI by auto
      ultimately have "A≲1" using eq_lepoll_trans by auto
      then have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" using linord_spectrum
        by auto
    }
    ultimately have "A{is in the spectrum of}(λT. IsLinOrder(T,{⟨U,V⟩∈Pow(⋃T)×Pow(⋃T). U⊆V}))" by blast
  }
  then show "T{is anti-}(λT. IsLinOrder(T, {⟨U,V⟩ ∈ Pow(⋃T) × Pow(⋃T) . U ⊆ V}))" unfolding antiProperty_def
    by auto
qed

text‹In conclusion, $T_1$ is also an anti-property.›

text‹Let's define some anti-properties that we'll use in the future.›

definition
  IsAntiComp ("_{is anti-compact}")
  where "T{is anti-compact} ≡ T{is anti-}(λT. (⋃T){is compact in}T)"

definition
  IsAntiLin ("_{is anti-lindeloef}")
  where "T{is anti-lindeloef} ≡ T{is anti-}(λT. ((⋃T){is lindeloef in}T))"

text‹Anti-compact spaces are also called pseudo-finite spaces in literature
before the concept of anti-property was defined.›

end