Theory Topology_ZF_11

(* 
    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 ‹Topology 11›

theory Topology_ZF_11 imports Topology_ZF_7 Finite_ZF_1

begin

text‹This file deals with order topologies. The order topology
is already defined in @{file "Topology_ZF_examples_1.thy"}.›

subsection‹Order topologies›

text‹We will assume
most of the time that the ordered set has more than one point.
It is natural to think that the topological properties
can be translated to properties of the order; since every
order rises one and only one topology in a set.›

subsection‹Separation properties›

text‹Order topologies have a lot of separation properties.›

text‹Every order topology is Hausdorff.›

theorem order_top_T2:
  assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X"
  shows "(OrdTopology X r){is T⇩2}"
proof-
  {
    fix x y assume A1:"x∈⋃(OrdTopology X r)""y∈⋃(OrdTopology X r)""x≠y"
    then have AS:"x∈X""y∈X""x≠y" using union_ordtopology[OF assms(1) assms(2)] by auto
    {
      assume A2:"∃z∈X-{x,y}. (⟨x,y⟩∈r⟶⟨x,z⟩∈r∧⟨z,y⟩∈r)∧(⟨y,x⟩∈r⟶⟨y,z⟩∈r∧⟨z,x⟩∈r)"
      from AS(1,2) assms(1) have "⟨x,y⟩∈r∨⟨y,x⟩∈r" unfolding IsLinOrder_def IsTotal_def by auto moreover
      {
        assume "⟨x,y⟩∈r"
        with AS A2 obtain z where z:"⟨x,z⟩∈r""⟨z,y⟩∈r""z∈X""z≠x""z≠y" by auto
        with AS(1,2) have "x∈LeftRayX(X,r,z)""y∈RightRayX(X,r,z)" unfolding LeftRayX_def RightRayX_def
          by auto moreover
        have "LeftRayX(X,r,z)∩RightRayX(X,r,z)=0" using inter_lray_rray[OF z(3) z(3) assms(1)]
          unfolding IntervalX_def using Order_ZF_2_L4[OF total_is_refl _ z(3)] assms(1) unfolding IsLinOrder_def
          by auto moreover
        have "LeftRayX(X,r,z)∈(OrdTopology X r)""RightRayX(X,r,z)∈(OrdTopology X r)"
          using z(3) base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
        ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
      }
      moreover
      {
        assume "⟨y,x⟩∈r"
        with AS A2 obtain z where z:"⟨y,z⟩∈r""⟨z,x⟩∈r""z∈X""z≠x""z≠y" by auto
        with AS(1,2) have "y∈LeftRayX(X,r,z)""x∈RightRayX(X,r,z)" unfolding LeftRayX_def RightRayX_def
          by auto moreover
        have "LeftRayX(X,r,z)∩RightRayX(X,r,z)=0" using inter_lray_rray[OF z(3) z(3) assms(1)]
          unfolding IntervalX_def using Order_ZF_2_L4[OF total_is_refl _ z(3)] assms(1) unfolding IsLinOrder_def
          by auto moreover
        have "LeftRayX(X,r,z)∈(OrdTopology X r)""RightRayX(X,r,z)∈(OrdTopology X r)"
          using z(3) base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
        ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
      }
      ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
    }
    moreover
    {
      assume A2:"∀z∈X - {x, y}. (⟨x, y⟩ ∈ r ∧ (⟨x, z⟩ ∉ r ∨ ⟨z, y⟩ ∉ r)) ∨ (⟨y, x⟩ ∈ r ∧ (⟨y, z⟩ ∉ r ∨ ⟨z, x⟩ ∉ r))"
      from AS(1,2) assms(1) have disj:"⟨x,y⟩∈r∨⟨y,x⟩∈r" unfolding IsLinOrder_def IsTotal_def by auto moreover
      {
        assume TT:"⟨x,y⟩∈r"
        with AS assms(1) have T:"⟨y,x⟩∉r" unfolding IsLinOrder_def antisym_def by auto
        from TT AS(1-3) have "x∈LeftRayX(X,r,y)""y∈RightRayX(X,r,x)" unfolding LeftRayX_def RightRayX_def
          by auto moreover
        {
          fix z assume "z∈LeftRayX(X,r,y)∩RightRayX(X,r,x)"
          then have "⟨z,y⟩∈r""⟨x,z⟩∈r""z∈X-{x,y}" unfolding RightRayX_def LeftRayX_def by auto
          with A2 T have "False" by auto
        }
        then have "LeftRayX(X,r,y)∩RightRayX(X,r,x)=0" by auto moreover
        have "LeftRayX(X,r,y)∈(OrdTopology X r)""RightRayX(X,r,x)∈(OrdTopology X r)"
          using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] AS by auto
        ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
      }
      moreover
      {
        assume TT:"⟨y,x⟩∈r"
        with AS assms(1) have T:"⟨x,y⟩∉r" unfolding IsLinOrder_def antisym_def by auto
        from TT AS(1-3) have "y∈LeftRayX(X,r,x)""x∈RightRayX(X,r,y)" unfolding LeftRayX_def RightRayX_def
          by auto moreover
        {
          fix z assume "z∈LeftRayX(X,r,x)∩RightRayX(X,r,y)"
          then have "⟨z,x⟩∈r""⟨y,z⟩∈r""z∈X-{x,y}" unfolding RightRayX_def LeftRayX_def by auto
          with A2 T have "False" by auto
        }
        then have "LeftRayX(X,r,x)∩RightRayX(X,r,y)=0" by auto moreover
        have "LeftRayX(X,r,x)∈(OrdTopology X r)""RightRayX(X,r,y)∈(OrdTopology X r)"
          using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] AS by auto
        ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
      }
      ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
    }
    ultimately have "∃U∈(OrdTopology X r). ∃V∈(OrdTopology X r). x∈U ∧ y∈V ∧ U∩V=0" by auto
  }
  then show ?thesis unfolding isT2_def by auto
qed

text‹Every order topology is $T_4$, but the proof needs lots of machinery.
At the end of the file, we will prove that every order topology is normal; sooner
or later.›

subsection‹Connectedness properties›

text‹Connectedness is related to two properties of orders: completeness and density›

text‹Some order-dense properties:›

definition
  IsDenseSub ("_ {is dense in}_{with respect to}_") where
  "A {is dense in}X{with respect to}r ≡ 
  ∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y  ⟶ (∃z∈A-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"

definition
  IsDenseUnp ("_ {is not-properly dense in}_{with respect to}_") where
  "A {is not-properly dense in}X{with respect to}r ≡ 
  ∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y  ⟶ (∃z∈A. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"

definition
  IsWeaklyDenseSub ("_ {is weakly dense in}_{with respect to}_") where
  "A {is weakly dense in}X{with respect to}r ≡ 
  ∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y  ⟶ ((∃z∈A-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)∨ IntervalX(X,r,x,y)=0)"

definition
  IsDense ("_ {is dense with respect to}_") where
  "X {is dense with respect to}r ≡ 
  ∀x∈X. ∀y∈X. ⟨x,y⟩∈r ∧ x≠y  ⟶ (∃z∈X-{x,y}. ⟨x,z⟩∈r∧⟨z,y⟩∈r)"

lemma dense_sub:
  shows "(X {is dense with respect to}r) ⟷ (X {is dense in}X{with respect to}r)"
  unfolding IsDenseSub_def IsDense_def by auto

lemma not_prop_dense_sub:
  shows "(A {is dense in}X{with respect to}r) ⟶ (A {is not-properly dense in}X{with respect to}r)"
  unfolding IsDenseSub_def IsDenseUnp_def by auto

text‹In densely ordered sets, intervals are infinite.›

theorem dense_order_inf_intervals:
  assumes "IsLinOrder(X,r)" "IntervalX(X, r, b, c)≠0""b∈X""c∈X" "X{is dense with respect to}r"
  shows "¬Finite(IntervalX(X, r, b, c))"
proof
  assume fin:"Finite(IntervalX(X, r, b, c))"
  have sub:"IntervalX(X, r, b, c)⊆X" unfolding IntervalX_def by auto
  have p:"Minimum(r,IntervalX(X, r, b, c))∈IntervalX(X, r, b, c)" using Finite_ZF_1_T2(2)[OF assms(1) Finite_Fin[OF fin sub] assms(2)]
    by auto
  then have "⟨b,Minimum(r,IntervalX(X, r, b, c))⟩∈r""b≠Minimum(r,IntervalX(X, r, b, c))"
    unfolding IntervalX_def using Order_ZF_2_L1 by auto
  with assms(3,5) sub p obtain z1 where z1:"z1∈X""z1≠b""z1≠Minimum(r,IntervalX(X, r, b, c))""⟨b,z1⟩∈r""⟨z1,Minimum(r,IntervalX(X, r, b, c))⟩∈r"
    unfolding IsDense_def by blast
  from p have B:"⟨Minimum(r,IntervalX(X, r, b, c)),c⟩∈r" unfolding IntervalX_def using Order_ZF_2_L1 by auto moreover
  have "trans(r)" using assms(1) unfolding IsLinOrder_def by auto moreover
  note z1(5) ultimately have z1a:"⟨z1,c⟩∈r" unfolding trans_def by fast
  {
    assume "z1=c"
    with B have "⟨Minimum(r,IntervalX(X, r, b, c)),z1⟩∈r" by auto
    with z1(5) have "z1=Minimum(r,IntervalX(X, r, b, c))" using assms(1) unfolding IsLinOrder_def antisym_def by auto
    then have "False" using z1(3) by auto
  }
  then have "z1≠c" by auto
  with z1(1,2,4) z1a have "z1∈IntervalX(X, r, b, c)" unfolding IntervalX_def using Order_ZF_2_L1 by auto
  then have "⟨Minimum(r,IntervalX(X, r, b, c)),z1⟩∈r" using Finite_ZF_1_T2(4)[OF assms(1) Finite_Fin[OF fin sub] assms(2)] by auto
  with z1(5) have "z1=Minimum(r,IntervalX(X, r, b, c))" using assms(1) unfolding IsLinOrder_def antisym_def by auto
  with z1(3) show "False" by auto
qed

text‹Left rays are infinite.›

theorem dense_order_inf_lrays:
  assumes "IsLinOrder(X,r)" "LeftRayX(X,r,c)≠0""c∈X"  "X{is dense with respect to}r"
  shows "¬Finite(LeftRayX(X,r,c))"
proof-
  from assms(2) obtain b where "b∈X""⟨b,c⟩∈r""b≠c" unfolding LeftRayX_def by auto
  with assms(3) obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" using assms(4) 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 nFIN:"¬Finite(IntervalX(X, r, b, c))" using dense_order_inf_intervals[OF assms(1) _ _ assms(3,4)]
    ‹b∈X› by auto
  {
    fix d assume "d∈IntervalX(X, r, b, c)"
    then have "⟨b,d⟩∈r""⟨d,c⟩∈r""d∈X""d≠b""d≠c" unfolding IntervalX_def using Order_ZF_2_L1 by auto
    then have "d∈LeftRayX(X,r,c)" unfolding LeftRayX_def by auto
  }
  then have "IntervalX(X, r, b, c)⊆LeftRayX(X,r,c)" by auto
  with nFIN show ?thesis using subset_Finite by auto
qed

text‹Right rays are infinite.›

theorem dense_order_inf_rrays:
  assumes "IsLinOrder(X,r)" "RightRayX(X,r,b)≠0""b∈X"  "X{is dense with respect to}r"
  shows "¬Finite(RightRayX(X,r,b))"
proof-
  from assms(2) obtain c where "c∈X""⟨b,c⟩∈r""b≠c" unfolding RightRayX_def by auto
  with assms(3) obtain z where "z∈X-{b,c}""⟨b,z⟩∈r""⟨z,c⟩∈r" using assms(4) 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 nFIN:"¬Finite(IntervalX(X, r, b, c))" using dense_order_inf_intervals[OF assms(1) _ assms(3) _ assms(4)]
    ‹c∈X› by auto
  {
    fix d assume "d∈IntervalX(X, r, b, c)"
    then have "⟨b,d⟩∈r""⟨d,c⟩∈r""d∈X""d≠b""d≠c" unfolding IntervalX_def using Order_ZF_2_L1 by auto
    then have "d∈RightRayX(X,r,b)" unfolding RightRayX_def by auto
  }
  then have "IntervalX(X, r, b, c)⊆RightRayX(X,r,b)" by auto
  with nFIN show ?thesis using subset_Finite by auto
qed

text‹The whole space in a densely ordered set is infinite.›

corollary dense_order_infinite:
  assumes "IsLinOrder(X,r)"  "X{is dense with respect to}r"
    "∃x y. x≠y∧x∈X∧y∈X"
  shows "¬(X≺nat)"
proof-
  from assms(3) obtain b c where B:"b∈X""c∈X""b≠c" by auto
  {
    assume "⟨b,c⟩∉r"
    with assms(1) have "⟨c,b⟩∈r" unfolding IsLinOrder_def IsTotal_def using ‹b∈X›‹c∈X› by auto
    with assms(2) 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(1) _ ‹c∈X›‹b∈X› assms(2)]
      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(2) 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(1) _ ‹b∈X›‹c∈X› assms(2)]
      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 show ?thesis by auto
qed

text‹If an order topology is connected, then the order is complete.
It is equivalent to assume that $r\subseteq X\times X$ or prove that
$r\cap X\times X$ is complete.›

theorem conn_imp_complete:
  assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X" "r⊆X×X"
     "(OrdTopology X r){is connected}"
  shows "r{is complete}"
proof-
  {
    assume "¬(r{is complete})"
    then obtain A where A:"A≠0""IsBoundedAbove(A,r)""¬(HasAminimum(r, ⋂b∈A. r `` {b}))" unfolding
      IsComplete_def by auto
    from A(3) have r1:"∀m∈⋂b∈A. r `` {b}. ∃x∈⋂b∈A. r `` {b}. ⟨m,x⟩∉r" unfolding HasAminimum_def
      by force
    from A(1,2) obtain b where r2:"∀x∈A. ⟨x, b⟩ ∈ r" unfolding IsBoundedAbove_def by auto
    with assms(3) A(1) have "A⊆X""b∈X" by auto
    with assms(3) have r3:"∀c∈A. r `` {c}⊆X" using image_iff by auto
    from r2 have "∀x∈A. b∈r``{x}" using image_iff by auto
    then have noE:"b∈(⋂b∈A. r `` {b})" using A(1) by auto
    {
      fix x assume "x∈(⋂b∈A. r `` {b})"
      then have "∀c∈A. x∈r``{c}" by auto
      with A(1) obtain c where "c∈A" "x∈r``{c}" by auto
      with r3 have "x∈X" by auto
    }
    then have sub:"(⋂b∈A. r `` {b})⊆X" by auto
    {
      fix x assume x:"x∈(⋂b∈A. r `` {b})"
      with r1 have "∃z∈⋂b∈A. r `` {b}. ⟨x,z⟩∉r" by auto
      then obtain z where z:"z∈(⋂b∈A. r `` {b})""⟨x,z⟩∉r" by auto
      from x z(1) sub have "x∈X""z∈X" by auto
      with z(2) have "⟨z,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def by auto
      then have xx:"x∈RightRayX(X,r,z)" unfolding RightRayX_def using ‹x∈X›‹⟨x,z⟩∉r›
        assms(1) unfolding IsLinOrder_def using total_is_refl unfolding refl_def by auto
      {
        fix m assume "m∈RightRayX(X,r,z)"
        then have m:"m∈X-{z}""⟨z,m⟩∈r" unfolding RightRayX_def by auto
        {
          fix c assume "c∈A"
          with z(1) have "⟨c,z⟩∈r" using image_iff by auto
          with m(2) have "⟨c,m⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
          then have "m∈r``{c}" using image_iff by auto
        }
        with A(1) have "m∈(⋂b∈A. r `` {b})" by auto
      }
      then have sub1:"RightRayX(X,r,z)⊆(⋂b∈A. r `` {b})" by auto
      have "RightRayX(X,r,z)∈(OrdTopology X r)" using 
        base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] ‹z∈X› by auto
      with sub1 xx have "∃U∈(OrdTopology X r). x∈U ∧ U⊆(⋂b∈A. r `` {b})" by auto
    }
    then have "(⋂b∈A. r `` {b})∈(OrdTopology X r)" using topology0.open_neigh_open[OF topology0_ordtopology[OF assms(1)]]
      by auto moreover
    {
      fix x assume "x∈X-(⋂b∈A. r `` {b})"
      then have "x∈X""x∉(⋂b∈A. r `` {b})" by auto
      with A(1) obtain b where "x∉r``{b}""b∈A" by auto
      then have "⟨b,x⟩∉r" using image_iff by auto
      with ‹A⊆X› ‹b∈A›‹x∈X› have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def
        IsTotal_def by auto
      then have xx:"x∈LeftRayX(X,r,b)" unfolding LeftRayX_def using ‹x∈X› ‹⟨b,x⟩∉r›
        assms(1) unfolding IsLinOrder_def using total_is_refl unfolding refl_def by auto
      {
        fix y assume "y∈LeftRayX(X,r,b)∩(⋂b∈A. r `` {b})"
        then have "y∈X-{b}""⟨y,b⟩∈r""∀c∈A. y∈r``{c}" unfolding LeftRayX_def by auto
        then have "y∈X""⟨y,b⟩∈r""∀c∈A. ⟨c,y⟩∈r" using image_iff by auto
        with ‹b∈A› have "y=b" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        then have "False" using ‹y∈X-{b}› by auto
      }
      then have sub1:"LeftRayX(X,r,b)⊆X-(⋂b∈A. r `` {b})" unfolding LeftRayX_def by auto
      have "LeftRayX(X,r,b)∈(OrdTopology X r)" using 
        base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] ‹b∈A›‹A⊆X› by blast
      with sub1 xx have "∃U∈(OrdTopology X r). x∈U∧U⊆X-(⋂b∈A. r `` {b})" by auto
    }
    then have "X - (⋂b∈A. r `` {b})∈(OrdTopology X r)" using topology0.open_neigh_open[OF topology0_ordtopology[OF assms(1)]]
      by auto
    then have "⋃(OrdTopology X r)-(⋂b∈A. r `` {b})∈(OrdTopology X r)" using union_ordtopology[OF assms(1,2)] by auto
    then have "(⋂b∈A. r `` {b}){is closed in}(OrdTopology X r)" unfolding IsClosed_def using union_ordtopology[OF assms(1,2)]
      sub by auto
    moreover note assms(4) ultimately
    have "(⋂b∈A. r `` {b})=0∨(⋂b∈A. r `` {b})=X" using union_ordtopology[OF assms(1,2)] unfolding IsConnected_def
      by auto
    then have e1:"(⋂b∈A. r `` {b})=X" using noE by auto
    then have "∀x∈X. ∀b∈A. x∈r``{b}" by auto
    then have r4:"∀x∈X. ∀b∈A. ⟨b,x⟩∈r" using image_iff by auto
    {
      fix a1 a2 assume aA:"a1∈A""a2∈A""a1≠a2"
      with ‹A⊆X› have aX:"a1∈X""a2∈X" by auto
      with r4 aA(1,2) have "⟨a1,a2⟩∈r""⟨a2,a1⟩∈r" by auto
      then have "a1=a2" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      with aA(3) have "False" by auto
    }
    moreover
    from A(1) obtain t where "t∈A" by auto
    ultimately have "A={t}" by auto
    with r4 have "∀x∈X. ⟨t,x⟩∈r""t∈X" using ‹A⊆X› by auto
    then have "HasAminimum(r,X)" unfolding HasAminimum_def by auto
    with e1 have "HasAminimum(r,⋂b∈A. r `` {b})" by auto
    with A(3) have "False" by auto
  }
  then show ?thesis by auto
qed

text‹If an order topology is connected, then the order is dense.›

theorem conn_imp_dense:
  assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X"
     "(OrdTopology X r){is connected}"
  shows "X {is dense with respect to}r"
proof-
  {
    assume "¬(X {is dense with respect to}r)"
    then have "∃x1∈X. ∃x2∈X. ⟨x1,x2⟩∈r∧x1≠x2∧(∀z∈X-{x1,x2}. ⟨x1,z⟩∉r∨⟨z,x2⟩∉r)"
      unfolding IsDense_def by auto
    then obtain x1 x2 where x:"x1∈X""x2∈X""⟨x1,x2⟩∈r""x1≠x2""(∀z∈X-{x1,x2}. ⟨x1,z⟩∉r∨⟨z,x2⟩∉r)" by auto
    from x(1,2) have P:"LeftRayX(X,r,x2)∈(OrdTopology X r)""RightRayX(X,r,x1)∈(OrdTopology X r)"
      using  base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
    {
      fix x assume "x∈X-LeftRayX(X,r,x2)"
      then have "x∈X" "x∉LeftRayX(X,r,x2)" by auto
      then have "⟨x,x2⟩∉r∨x=x2" unfolding LeftRayX_def by auto
      then have "⟨x2,x⟩∈r∨x=x2" using assms(1) ‹x∈X› ‹x2∈X› unfolding IsLinOrder_def
        IsTotal_def by auto
      then have s:"⟨x2,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl ‹x2∈X›
        unfolding refl_def by auto
      with x(3) have "⟨x1,x⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
      then have "x=x1∨x∈RightRayX(X,r,x1)" unfolding RightRayX_def using ‹x∈X› by auto
      with s have "⟨x2,x1⟩∈r∨x∈RightRayX(X,r,x1)" by auto
      with x(3) have "x1=x2 ∨ x∈RightRayX(X,r,x1)" using assms(1) unfolding IsLinOrder_def
        antisym_def by auto
      with x(4) have "x∈RightRayX(X,r,x1)" by auto
    }
    then have "X-LeftRayX(X,r,x2)⊆RightRayX(X,r,x1)" by auto moreover
    {
      fix x assume "x∈RightRayX(X,r,x1)"
      then have xr:"x∈X-{x1}""⟨x1,x⟩∈r" unfolding RightRayX_def by auto
      {
        assume "x∈LeftRayX(X,r,x2)"
        then have xl:"x∈X-{x2}""⟨x,x2⟩∈r" unfolding LeftRayX_def by auto
        from xl xr x(5) have "False" by auto
      }
      with xr(1) have "x∈X-LeftRayX(X,r,x2)" by auto
    }
    ultimately have "RightRayX(X,r,x1)=X-LeftRayX(X,r,x2)" by auto
    then have "LeftRayX(X,r,x2){is closed in}(OrdTopology X r)" using P(2) union_ordtopology[
      OF assms(1,2)] unfolding IsClosed_def LeftRayX_def by auto
    with P(1) have "LeftRayX(X,r,x2)=0∨LeftRayX(X,r,x2)=X" using union_ordtopology[
      OF assms(1,2)] assms(3) unfolding IsConnected_def by auto
    with x(1,3,4) have "LeftRayX(X,r,x2)=X" unfolding LeftRayX_def by auto
    then have "x2∈LeftRayX(X,r,x2)" using x(2) by auto
    then have "False" unfolding LeftRayX_def by auto
  }
  then show ?thesis by auto
qed

text‹Actually a connected order topology is one that comes from a dense
and complete order.›

text‹First a lemma. In a complete ordered set, every non-empty set bounded from below has
a maximum lower bound.›

lemma complete_order_bounded_below:
  assumes "r{is complete}" "IsBoundedBelow(A,r)" "A≠0" "r⊆X×X"
  shows "HasAmaximum(r,⋂c∈A. r-``{c})"
proof-
  let ?M="⋂c∈A. r-``{c}"
  from assms(3) obtain t where A:"t∈A" by auto
  {
    fix m assume "m∈?M"
    with A have "m∈r-``{t}" by auto
    then have "⟨m,t⟩∈r" by auto
  }
  then have "(∀x∈⋂c∈A. r -`` {c}. ⟨x, t⟩ ∈ r)" by auto
  then have "IsBoundedAbove(?M,r)" unfolding IsBoundedAbove_def by auto
  moreover
  from assms(2,3) obtain l where " ∀x∈A. ⟨l, x⟩ ∈ r" unfolding IsBoundedBelow_def by auto
  then have "∀x∈A. l ∈ r-``{x}" using vimage_iff by auto
  with assms(3) have "l∈?M" by auto
  then have "?M≠0" by auto moreover note assms(1)
  ultimately have "HasAminimum(r,⋂c∈?M. r `` {c})" unfolding IsComplete_def by auto
  then obtain rr where rr:"rr∈(⋂c∈?M. r `` {c})" "∀s∈(⋂c∈?M. r `` {c}). ⟨rr,s⟩∈r" unfolding HasAminimum_def
    by auto
  {
    fix aa assume A:"aa∈A"
    {
      fix c assume M:"c∈?M"
      with A have "⟨c,aa⟩∈r" by auto
      then have "aa∈r``{c}" by auto
    }
    then have "aa∈(⋂c∈?M. r `` {c})" using rr(1) by auto
  }
  then have "A⊆(⋂c∈?M. r `` {c})" by auto
  with rr(2) have "∀s∈A. ⟨rr,s⟩∈r" by auto
  then have "rr∈?M" using assms(3) by auto
  moreover
  {
    fix m assume "m∈?M"
    then have "rr∈r``{m}" using rr(1) by auto
    then have "⟨m,rr⟩∈r" by auto
  }
  then have "∀m∈?M. ⟨m,rr⟩∈r" by auto
  ultimately show ?thesis unfolding HasAmaximum_def by auto
qed 

theorem comp_dense_imp_conn:
  assumes "IsLinOrder(X,r)" "∃x y. x≠y∧x∈X∧y∈X" "r⊆X×X"
     "X {is dense with respect to}r" "r{is complete}"
  shows "(OrdTopology X r){is connected}"
proof-
  {
    assume "¬((OrdTopology X r){is connected})"
    then obtain U where U:"U≠0""U≠X""U∈(OrdTopology X r)""U{is closed in}(OrdTopology X r)"
      unfolding IsConnected_def using union_ordtopology[OF assms(1,2)] by auto
    from U(4) have A:"X-U∈(OrdTopology X r)""U⊆X" unfolding IsClosed_def using union_ordtopology[OF assms(1,2)] by auto
    from U(1) obtain u where "u∈U" by auto
    from A(2) U(1,2) have "X-U≠0" by auto
    then obtain v where "v∈X-U" by auto
    with ‹u∈U› ‹U⊆X› have "⟨u,v⟩∈r∨⟨v,u⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
      by auto
    {
      assume "⟨u,v⟩∈r"
      have "LeftRayX(X,r,v)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
        ‹v∈X-U› by auto
      then have "U∩LeftRayX(X,r,v)∈(OrdTopology X r)" using U(3) using Ordtopology_is_a_topology(1)
        [OF assms(1)] unfolding IsATopology_def by auto
      {
        fix b assume "b∈(U)∩LeftRayX(X,r,v)"
        then have "⟨b,v⟩∈r" unfolding LeftRayX_def by auto
      }
      then have bound:"IsBoundedAbove(U∩LeftRayX(X,r,v),r)" unfolding IsBoundedAbove_def by auto moreover
      with ‹⟨u,v⟩∈r›‹u∈U›‹U⊆X›‹v∈X-U› have nE:"U∩LeftRayX(X,r,v)≠0" unfolding LeftRayX_def by auto
      ultimately have Hmin:"HasAminimum(r,⋂c∈U∩LeftRayX(X,r,v). r``{c})" using assms(5) unfolding IsComplete_def
        by auto
      let ?min="Supremum(r,U∩LeftRayX(X,r,v))"
      {
        fix c assume "c∈U∩LeftRayX(X,r,v)"
        then have "⟨c,v⟩∈r" unfolding LeftRayX_def by auto
      }
      then have a1:"⟨?min,v⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def
        by auto
      {
        assume ass:"?min∈U"
        then obtain V where V:"?min∈V""V⊆U"
          "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
          [OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹U∈(OrdTopology X r)› ass] by blast
        {
          assume "V∈{RightRayX(X,r,b). b∈X}"
          then obtain b where b:"b∈X" "V=RightRayX(X,r,b)" by auto
          note a1 moreover
          from V(1) b(2) have a2:"⟨b,?min⟩∈r""?min≠b" unfolding RightRayX_def by auto
          ultimately have "⟨b,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by blast moreover
          {
            assume "b=v"
            with a1 a2(1) have "b=?min" using assms(1) unfolding IsLinOrder_def antisym_def by auto
            with a2(2) have "False" by auto
          }
          ultimately have "False" using V(2) b(2) unfolding RightRayX_def using ‹v∈X-U› by auto
        }
        moreover
        {
          assume "V∈{LeftRayX(X,r,b). b∈X}"
          then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
          {
            assume "⟨v,b⟩∈r"
            then have "b=v∨v∈LeftRayX(X,r,b)" unfolding LeftRayX_def using ‹v∈X-U› by auto
            then have "b=v" using b(1) V(2) ‹v∈X-U› by auto
          }
          then have bv:"⟨b,v⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def using b(2)
            ‹v∈X-U› by auto
          from b(1) V(1) have "⟨?min,b⟩∈r""?min≠b" unfolding LeftRayX_def by auto
          with assms(4) obtain z where z:"⟨?min,z⟩∈r""⟨z,b⟩∈r""z∈X-{b,?min}" unfolding IsDense_def
            using b(2) V(1,2) ‹U⊆X› by blast
          then have rayb:"z∈LeftRayX(X,r,b)" unfolding LeftRayX_def by auto
          from z(2) bv have "⟨z,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
          moreover
          {
            assume "z=v"
            with bv have "⟨b,z⟩∈r" by auto
            with z(2) have "b=z" using assms(1) unfolding IsLinOrder_def antisym_def by auto
            then have "False" using z(3) by auto
          }
          ultimately have "z∈LeftRayX(X,r,v)" unfolding LeftRayX_def using z(3) by auto
          with rayb have "z∈U∩LeftRayX(X,r,v)" using V(2) b(1) by auto
          then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
            by auto
          then have "⟨z,?min⟩∈r" by auto
          with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        }
        moreover
        {
          assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
          then obtain b c where b:"V=IntervalX(X,r,b,c)" "b∈X""c∈X" by auto
          from b V(1) have m:"⟨?min,c⟩∈r""⟨b,?min⟩∈r""?min≠b" "?min≠c" unfolding IntervalX_def Interval_def by auto  
          {
            assume A:"⟨c,v⟩∈r"
            from m obtain z where z:"⟨z,c⟩∈r" "⟨?min,z⟩∈r""z∈X-{c,?min}" using assms(4) unfolding IsDense_def
              using b(3) V(1,2) ‹U⊆X› by blast
            from z(2) have "⟨b,z⟩∈r" using m(2) assms(1) unfolding IsLinOrder_def trans_def
              by fast
            with z(1) have "z∈IntervalX(X,r,b,c)∨z=b" using z(3) unfolding IntervalX_def
              Interval_def by auto
            then have "z∈IntervalX(X,r,b,c)" using m(2) z(2,3) using assms(1) unfolding IsLinOrder_def
              antisym_def by auto
            with b(1) V(2) have "z∈U" by auto moreover
            from A z(1) have "⟨z,v⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
            moreover have "z≠v" using A z(1,3) assms(1) unfolding IsLinOrder_def antisym_def by auto
            ultimately have "z∈U∩LeftRayX(X,r,v)" unfolding LeftRayX_def using z(3) by auto
            then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
              by auto
            then have "⟨z,?min⟩∈r" by auto
            with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
          }
          then have vc:"⟨v,c⟩∈r""v≠c" using assms(1) unfolding IsLinOrder_def IsTotal_def using ‹v∈X-U›
            b(3) by auto
          {
            assume "?min=v"
            with V(2,1) ‹v∈X-U› have "False" by auto
          }
          then have "?min≠v" by auto
          with a1 obtain z where z:"⟨?min,z⟩∈r""⟨z,v⟩∈r""z∈X-{?min,v}" using assms(4) unfolding IsDense_def
            using V(1,2) ‹U⊆X›‹v∈X-U› by blast
          from z(2) vc(1) have zc:"⟨z,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
            by fast moreover
          from m(2) z(1) have "⟨b,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
            by fast ultimately
          have "z∈Interval(r,b,c)" using Order_ZF_2_L1B by auto moreover
          {
            assume "z=c"
            then have "False" using z(2) vc using assms(1) unfolding IsLinOrder_def antisym_def
              by fast
          }
          then have "z≠c" by auto moreover
          {
            assume "z=b"
            then have "z=?min" using m(2) z(1) using assms(1) unfolding IsLinOrder_def
              antisym_def by auto
            with z(3) have "False" by auto
          }
          then have "z≠b" by auto moreover
          have "z∈X" using z(3) by auto ultimately
          have "z∈IntervalX(X,r,b,c)" unfolding IntervalX_def by auto
          then have "z∈V" using b(1) by auto
          then have "z∈U" using V(2) by auto moreover
          from z(2,3) have "z∈LeftRayX(X,r,v)" unfolding LeftRayX_def by auto ultimately
          have "z∈U∩LeftRayX(X,r,v)" by auto
          then have "?min∈r``{z}" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
            by auto
          then have "⟨z,?min⟩∈r" by auto
          with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        }
        ultimately have "False" using V(3) by auto
      }
      then have ass:"?min∈X-U" using a1 assms(3) by auto
      then obtain V where V:"?min∈V""V⊆X-U"
        "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
        [OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹X-U∈(OrdTopology X r)› ass] by blast
      {
        assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
        then obtain b c where b:"V=IntervalX(X,r,b,c)""b∈X""c∈X" by auto
        from b V(1) have m:"⟨?min,c⟩∈r""⟨b,?min⟩∈r""?min≠b" "?min≠c" unfolding IntervalX_def Interval_def by auto  
        {
          fix x assume A:"x∈U∩LeftRayX(X,r,v)"
          then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
          then have "x∉V" using V(2) by auto
          then have "x∉Interval(r, b, c) ∩ X∨x=b∨x=c" using b(1) unfolding IntervalX_def by auto
          then have "(⟨b,x⟩∉r∨⟨x,c⟩∉r)∨x=b∨x=c""x∈X" using Order_ZF_2_L1B ‹x∈U›‹U⊆X› by auto
          then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)∨x=b∨x=c" using assms(1) unfolding IsLinOrder_def IsTotal_def
            using b(2,3) by auto
          then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def using total_is_refl
            unfolding refl_def using b(2,3) by auto moreover
          from A have "⟨x,?min⟩∈r" using Order_ZF_4_L4(1)[OF _ Hmin] assms(1) unfolding Supremum_def IsLinOrder_def
            by auto
          ultimately have "(⟨x,b⟩∈r∨⟨c,?min⟩∈r)" using assms(1) unfolding IsLinOrder_def trans_def
            by fast
          with m(1) have "(⟨x,b⟩∈r∨c=?min)" using assms(1) unfolding IsLinOrder_def antisym_def by auto
          with m(4) have "⟨x,b⟩∈r" by auto
        }
        then have "⟨?min,b⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def by auto
        with m(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      }
      moreover
      {
        assume "V∈{RightRayX(X,r,b). b∈X}"
        then obtain b where b:"V=RightRayX(X,r,b)" "b∈X" by auto
        from b V(1) have m:"⟨b,?min⟩∈r""?min≠b" unfolding RightRayX_def by auto
        {
          fix x assume A:"x∈U∩LeftRayX(X,r,v)"
          then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
          then have "x∉V" using V(2) by auto
          then have "x∉RightRayX(X,r, b)" using b(1) by auto
          then have "(⟨b,x⟩∉r∨x=b)""x∈X" unfolding RightRayX_def using ‹x∈U›‹U⊆X› by auto
          then have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
            refl_def unfolding IsTotal_def using b(2) by auto
        }
        then have "⟨?min,b⟩∈r" using Order_ZF_5_L3[OF _ nE Hmin] assms(1) unfolding IsLinOrder_def by auto
        with m(2,1) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      } moreover
      {
         assume "V∈{LeftRayX(X,r,b). b∈X}"
        then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
        from b V(1) have m:"⟨?min,b⟩∈r""?min≠b" unfolding LeftRayX_def by auto
        {
          fix x assume A:"x∈U∩LeftRayX(X,r,v)"
          then have "⟨x,v⟩∈r""x∈U" unfolding LeftRayX_def by auto
          then have "x∉V" using V(2) by auto
          then have "x∉LeftRayX(X,r, b)" using b(1) by auto
          then have "(⟨x,b⟩∉r∨x=b)""x∈X" unfolding LeftRayX_def using ‹x∈U›‹U⊆X› by auto
          then have "⟨b,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
            refl_def unfolding IsTotal_def using b(2) by auto
          with m(1) have "⟨?min,x⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
          moreover 
          from bound A have "∃g. ∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" using nE
            unfolding IsBoundedAbove_def by auto
          then obtain g where g:"∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" by auto
          with nE obtain t where "t∈U∩LeftRayX(X,r,v)" by auto
          with g have "⟨t,g⟩∈r" by auto
          with assms(3) have "g∈X" by auto
          with g have boundX:"∃g∈X. ∀y∈U∩LeftRayX(X,r,v). ⟨y,g⟩∈r" by auto
          have "⟨x,?min⟩∈r" using Order_ZF_5_L7(2)[OF assms(3) _ assms(5) _ nE boundX]
            assms(1) ‹U⊆X› A unfolding LeftRayX_def IsLinOrder_def by auto
          ultimately have "x=?min" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        }
        then have "U∩LeftRayX(X,r,v)⊆{?min}" by auto moreover
        {
          assume "?min∈U∩LeftRayX(X,r,v)"
          then have "?min∈U" by auto
          then have "False" using V(1,2) by auto
        }
        ultimately have "False" using nE by auto
      }
      moreover note V(3)
      ultimately have "False" by auto
    }
    with assms(1) have "⟨v,u⟩∈r" unfolding IsLinOrder_def IsTotal_def using ‹u∈U›‹U⊆X›
      ‹v∈X-U› by auto
    have "RightRayX(X,r,v)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
      ‹v∈X-U› by auto
    then have "U∩RightRayX(X,r,v)∈(OrdTopology X r)" using U(3) using Ordtopology_is_a_topology(1)
      [OF assms(1)] unfolding IsATopology_def by auto
    {
      fix b assume "b∈(U)∩RightRayX(X,r,v)"
      then have "⟨v,b⟩∈r" unfolding RightRayX_def by auto
    }
    then have bound:"IsBoundedBelow(U∩RightRayX(X,r,v),r)" unfolding IsBoundedBelow_def by auto
    with ‹⟨v,u⟩∈r›‹u∈U›‹U⊆X›‹v∈X-U› have nE:"U∩RightRayX(X,r,v)≠0" unfolding RightRayX_def by auto
    have Hmax:"HasAmaximum(r,⋂c∈U∩RightRayX(X,r,v). r-``{c})" using complete_order_bounded_below[OF assms(5) bound nE assms(3)].
    let ?max="Infimum(r,U∩RightRayX(X,r,v))"
    {
      fix c assume "c∈U∩RightRayX(X,r,v)"
      then have "⟨v,c⟩∈r" unfolding RightRayX_def by auto
    }
    then have a1:"⟨v,?max⟩∈r" using Order_ZF_5_L4[OF _ nE Hmax] assms(1) unfolding IsLinOrder_def
      by auto
    {
      assume ass:"?max∈U"
      then obtain V where V:"?max∈V""V⊆U"
        "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
        [OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹U∈(OrdTopology X r)› ass] by blast
      {
        assume "V∈{RightRayX(X,r,b). b∈X}"
        then obtain b where b:"b∈X" "V=RightRayX(X,r,b)" by auto
        from V(1) b(2) have a2:"⟨b,?max⟩∈r""?max≠b" unfolding RightRayX_def by auto
        {
          assume "⟨b,v⟩∈r"
          then have "b=v∨v∈RightRayX(X,r,b)" unfolding RightRayX_def using ‹v∈X-U› by auto
          then have "b=v" using b(2) V(2) ‹v∈X-U› by auto
        }
        then have bv:"⟨v,b⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def using b(1)
          ‹v∈X-U› by auto
        from a2 assms(4) obtain z where z:"⟨b,z⟩∈r""⟨z,?max⟩∈r""z∈X-{b,?max}" unfolding IsDense_def
          using b(1) V(1,2) ‹U⊆X› by blast
        then have rayb:"z∈RightRayX(X,r,b)" unfolding RightRayX_def by auto
        from z(1) bv have "⟨v,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast moreover
        {
          assume "z=v"
          with bv have "⟨z,b⟩∈r" by auto
          with z(1) have "b=z" using assms(1) unfolding IsLinOrder_def antisym_def by auto
          then have "False" using z(3) by auto
        }
        ultimately have "z∈RightRayX(X,r,v)" unfolding RightRayX_def using z(3) by auto
        with rayb have "z∈U∩RightRayX(X,r,v)" using V(2) b(2) by auto
        then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
          by auto
        then have "⟨?max,z⟩∈r" by auto
        with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      }
      moreover
      {
        assume "V∈{LeftRayX(X,r,b). b∈X}"
        then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
        note a1 moreover
        from V(1) b(1) have a2:"⟨?max,b⟩∈r""?max≠b" unfolding LeftRayX_def by auto
        ultimately have "⟨v,b⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by blast moreover
        {
          assume "b=v"
          with a1 a2(1) have "b=?max" using assms(1) unfolding IsLinOrder_def antisym_def by auto
          with a2(2) have "False" by auto
        }
        ultimately have "False" using V(2) b(1) unfolding LeftRayX_def using ‹v∈X-U› by auto
      }
      moreover
      {
        assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
        then obtain b c where b:"V=IntervalX(X,r,b,c)" "b∈X""c∈X" by auto
        from b V(1) have m:"⟨?max,c⟩∈r""⟨b,?max⟩∈r""?max≠b" "?max≠c" unfolding IntervalX_def Interval_def by auto  
        {
          assume A:"⟨v,b⟩∈r"
          from m obtain z where z:"⟨z,?max⟩∈r" "⟨b,z⟩∈r""z∈X-{b,?max}" using assms(4) unfolding IsDense_def
            using b(2) V(1,2) ‹U⊆X› by blast
          from z(1) have "⟨z,c⟩∈r" using m(1) assms(1) unfolding IsLinOrder_def trans_def
            by fast
          with z(2) have "z∈IntervalX(X,r,b,c)∨z=c" using z(3) unfolding IntervalX_def
            Interval_def by auto
          then have "z∈IntervalX(X,r,b,c)" using m(1) z(1,3) using assms(1) unfolding IsLinOrder_def
            antisym_def by auto
          with b(1) V(2) have "z∈U" by auto moreover
          from A z(2) have "⟨v,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
          moreover have "z≠v" using A z(2,3) assms(1) unfolding IsLinOrder_def antisym_def by auto
          ultimately have "z∈U∩RightRayX(X,r,v)" unfolding RightRayX_def using z(3) by auto
          then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
            by auto
          then have "⟨?max,z⟩∈r" by auto
          with z(1,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        }
        then have vc:"⟨b,v⟩∈r""v≠b" using assms(1) unfolding IsLinOrder_def IsTotal_def using ‹v∈X-U›
          b(2) by auto
        {
          assume "?max=v"
          with V(2,1) ‹v∈X-U› have "False" by auto
        }
        then have "v≠?max" by auto moreover
        note a1 moreover
        have "?max∈X" using V(1,2) ‹U⊆X› by auto
        moreover have "v∈X" using ‹v∈X-U› by auto
        ultimately obtain z where z:"⟨v,z⟩∈r""⟨z,?max⟩∈r""z∈X-{v,?max}" using assms(4) unfolding IsDense_def
          by auto
        from z(1) vc(1) have zc:"⟨b,z⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
          by fast moreover
        from m(1) z(2) have "⟨z,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def
          by fast ultimately
        have "z∈Interval(r,b,c)" using Order_ZF_2_L1B by auto moreover
        {
          assume "z=b"
          then have "False" using z(1) vc using assms(1) unfolding IsLinOrder_def antisym_def
            by fast
        }
        then have "z≠b" by auto moreover
        {
          assume "z=c"
          then have "z=?max" using m(1) z(2) using assms(1) unfolding IsLinOrder_def
            antisym_def by auto
          with z(3) have "False" by auto
        }
        then have "z≠c" by auto moreover
        have "z∈X" using z(3) by auto ultimately
        have "z∈IntervalX(X,r,b,c)" unfolding IntervalX_def by auto
        then have "z∈V" using b(1) by auto
        then have "z∈U" using V(2) by auto moreover
        from z(1,3) have "z∈RightRayX(X,r,v)" unfolding RightRayX_def by auto ultimately
        have "z∈U∩RightRayX(X,r,v)" by auto
        then have "?max∈r-``{z}" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
          by auto
        then have "⟨?max,z⟩∈r" by auto
        with z(2,3) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      }
      ultimately have "False" using V(3) by auto
    }
    then have ass:"?max∈X-U" using a1 assms(3) by auto
    then obtain V where V:"?max∈V""V⊆X-U"
      "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}∪{LeftRayX(X,r,b). b∈X}∪{RightRayX(X,r,b). b∈X}" using point_open_base_neigh
      [OF Ordtopology_is_a_topology(2)[OF assms(1)] ‹X-U∈(OrdTopology X r)› ass] by blast
    {
      assume "V∈{IntervalX(X,r,b,c). ⟨b,c⟩∈X×X}"
      then obtain b c where b:"V=IntervalX(X,r,b,c)""b∈X""c∈X" by auto
      from b V(1) have m:"⟨?max,c⟩∈r""⟨b,?max⟩∈r""?max≠b" "?max≠c" unfolding IntervalX_def Interval_def by auto  
      {
        fix x assume A:"x∈U∩RightRayX(X,r,v)"
        then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
        then have "x∉V" using V(2) by auto
        then have "x∉Interval(r, b, c) ∩ X∨x=b∨x=c" using b(1) unfolding IntervalX_def by auto
        then have "(⟨b,x⟩∉r∨⟨x,c⟩∉r)∨x=b∨x=c""x∈X" using Order_ZF_2_L1B ‹x∈U›‹U⊆X› by auto
        then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)∨x=b∨x=c" using assms(1) unfolding IsLinOrder_def IsTotal_def
          using b(2,3) by auto
        then have "(⟨x,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def using total_is_refl
          unfolding refl_def using b(2,3) by auto moreover
        from A have "⟨?max,x⟩∈r" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
          by auto
        ultimately have "(⟨?max,b⟩∈r∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def trans_def
          by fast
        with m(2) have "(?max=b∨⟨c,x⟩∈r)" using assms(1) unfolding IsLinOrder_def antisym_def by auto
        with m(3) have "⟨c,x⟩∈r" by auto
      }
      then have "⟨c,?max⟩∈r" using Order_ZF_5_L4[OF _ nE Hmax] assms(1) unfolding IsLinOrder_def by auto
      with m(1,4) have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
    }
    moreover
    {
      assume "V∈{RightRayX(X,r,b). b∈X}"
      then obtain b where b:"V=RightRayX(X,r,b)" "b∈X" by auto
      from b V(1) have m:"⟨b,?max⟩∈r""?max≠b" unfolding RightRayX_def by auto
      {
        fix x assume A:"x∈U∩RightRayX(X,r,v)"
        then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
        then have "x∉V" using V(2) by auto
        then have "x∉RightRayX(X,r, b)" using b(1) by auto
        then have "(⟨b,x⟩∉r∨x=b)""x∈X" unfolding RightRayX_def using ‹x∈U›‹U⊆X› by auto
        then have "⟨x,b⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
          refl_def unfolding IsTotal_def using b(2) by auto moreover
        from A have "⟨?max,x⟩∈r" using Order_ZF_4_L3(1)[OF _ Hmax] assms(1) unfolding Infimum_def IsLinOrder_def
          by auto ultimately
        have "⟨?max,b⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
        with m have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
      }
      then have "False" using nE by auto
    } moreover
    {
       assume "V∈{LeftRayX(X,r,b). b∈X}"
      then obtain b where b:"V=LeftRayX(X,r,b)" "b∈X" by auto
      from b V(1) have m:"⟨?max,b⟩∈r""?max≠b" unfolding LeftRayX_def by auto
      {
        fix x assume A:"x∈U∩RightRayX(X,r,v)"
        then have "⟨v,x⟩∈r""x∈U" unfolding RightRayX_def by auto
        then have "x∉V" using V(2) by auto
        then have "x∉LeftRayX(X,r, b)" using b(1) by auto
        then have "(⟨x,b⟩∉r∨x=b)""x∈X" unfolding LeftRayX_def using ‹x∈U›‹U⊆X› by auto
        then have "⟨b,x⟩∈r" using assms(1) unfolding IsLinOrder_def using total_is_refl unfolding
          refl_def unfolding IsTotal_def using b(2) by auto
        then have "b∈r-``{x}" by auto
      }
      with nE have "b∈(⋂c∈U∩RightRayX(X,r,v). r-``{c})" by auto
      then have "⟨b,?max⟩∈r" unfolding Infimum_def using Order_ZF_4_L3(2)[OF _ Hmax] assms(1)
        unfolding IsLinOrder_def by auto
      with m have "False" using assms(1) unfolding IsLinOrder_def antisym_def by auto
    }
    moreover note V(3)
    ultimately have "False" by auto
  } 
  then show ?thesis by auto
qed

subsection‹Numerability axioms›

text‹A $\kappa$-separable order topology is in relation with order density.›

text‹If an order topology has a subset $A$ which is topologically
dense, then that subset is weakly order-dense in $X$.›

lemma dense_top_imp_Wdense_ord:
  assumes "IsLinOrder(X,r)" "Closure(A,OrdTopology X r)=X" "A⊆X" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
  shows "A{is weakly dense in}X{with respect to}r"
proof-
  {
    fix r1 r2 assume "r1∈X""r2∈X""r1≠r2" "⟨r1,r2⟩∈r"
    then have "IntervalX(X,r,r1,r2)∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪
      {RightRayX(X, r, b) . b ∈ X}" by auto
    then have P:"IntervalX(X,r,r1,r2)∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
      by auto
    have "IntervalX(X,r,r1,r2)⊆X" unfolding IntervalX_def by auto
    then have int:"Closure(A,OrdTopology X r)∩IntervalX(X,r,r1,r2)=IntervalX(X,r,r1,r2)" using assms(2) by auto
    {
      assume "IntervalX(X,r,r1,r2)≠0"
      then have "A∩(IntervalX(X,r,r1,r2))≠0" using topology0.cl_inter_neigh[OF topology0_ordtopology[OF assms(1)] _ P , of "A"]
        using assms(3) union_ordtopology[OF assms(1,4)] int by auto
    }
    then have "(∃z∈A-{r1,r2}. ⟨r1,z⟩∈r∧⟨z,r2⟩∈r)∨IntervalX(X,r,r1,r2)=0" unfolding IntervalX_def
      Interval_def by auto
  }
  then show ?thesis unfolding IsWeaklyDenseSub_def by auto
qed

text‹Conversely, a weakly order-dense set is topologically dense if it is also considered
that: if there is a maximum or a minimum elements whose singletons are open, this points
have to be in $A$. In conclusion, weakly order-density is a property closed to topological density.›

text‹Another way to see this: Consider a weakly order-dense set $A$:
\begin{itemize}
\item If $X$ has a maximum and a minimum and $\{min,max\}$ is open: $A$ is topologically dense in $X\setminus\{min,max\}$, where $min$ is the minimum in $X$ and $max$ is the maximum in $X$.
\item If $X$ has a maximum, $\{max\}$ is open and $X$ has no minimum
  or $\{min\}$ isn't open: $A$ is topologically dense in $X\setminus\{max\}$, where $max$ is the maximum in $X$.
\item If $X$ has a minimum, $\{min\}$ is open and $X$ has no maximum
  or $\{max\}$ isn't open $A$ is topologically dense in $X\setminus\{min\}$, where $min$ is the minimum in $X$.
\item If $X$ has no minimum or maximum, or $\{min,max\}$ has no proper open sets: $A$ is topologically dense in $X$.
\end{itemize}
›

lemma Wdense_ord_imp_dense_top:
  assumes "IsLinOrder(X,r)" "A{is weakly dense in}X{with respect to}r" "A⊆X" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
    "HasAminimum(r,X)⟶{Minimum(r,X)}∈(OrdTopology X r)⟶Minimum(r,X)∈A"
    "HasAmaximum(r,X)⟶{Maximum(r,X)}∈(OrdTopology X r)⟶Maximum(r,X)∈A"
  shows "Closure(A,OrdTopology X r)=X"
proof-
  {
    fix x assume "x∈X"
  {
    fix U assume ass:"x∈U""U∈(OrdTopology X r)"
    then have "∃V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X} . V⊆U∧x∈V"
      using point_open_base_neigh[OF Ordtopology_is_a_topology(2)[OF assms(1)]] by auto
    then obtain V where V:"V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X} ∪ {LeftRayX(X, r, b) . b ∈ X} ∪ {RightRayX(X, r, b) . b ∈ X}" "V⊆U" "x∈V"
      by blast
    note V(1) moreover
    {
      assume "V∈{IntervalX(X, r, b, c) . ⟨b,c⟩ ∈ X × X}"
      then obtain b c where b:"b∈X""c∈X""V=IntervalX(X, r, b, c)" by auto
      with V(3) have x:"⟨b,x⟩∈r" "⟨x,c⟩∈r" "x≠b" "x≠c" unfolding IntervalX_def Interval_def by auto
      then have "⟨b,c⟩∈r" using assms(1) unfolding IsLinOrder_def trans_def by fast
      moreover from x(1-3) have "b≠c" using assms(1) unfolding IsLinOrder_def antisym_def by fast
      moreover note assms(2) b V(3)
      ultimately have "∃z∈A-{b,c}. ⟨b,z⟩∈r∧⟨z,c⟩∈r" unfolding IsWeaklyDenseSub_def by auto
      then obtain z where "z∈A""z≠b""z≠c""⟨b,z⟩∈r""⟨z,c⟩∈r" by auto
      with assms(3) have "z∈A""z∈IntervalX(X, r, b, c)" unfolding IntervalX_def Interval_def by auto
      then have "A∩U≠0" using V(2) b(3) by auto
    }
    moreover
    {
      assume "V∈{RightRayX(X, r, b) . b ∈ X}"
      then obtain b where b:"b∈X""V=RightRayX(X, r, b)" by auto
      with V(3) have x:"⟨b,x⟩∈r" "b≠x" unfolding RightRayX_def by auto moreover
      note b(1) moreover
      have "U⊆⋃(OrdTopology X r)" using ass(2) by auto
      then have "U⊆X" using union_ordtopology[OF assms(1,4)] by auto
      then have "x∈X" using ass(1) by auto moreover
      note assms(2) ultimately
      have disj:"(∃z∈A-{b,x}. ⟨b,z⟩∈r∧⟨z,x⟩∈r)∨ IntervalX(X, r, b, x) = 0" unfolding IsWeaklyDenseSub_def by auto
      {
        assume B:"IntervalX(X, r, b, x) = 0"
        {
          assume "∃y∈X. ⟨x,y⟩∈r ∧ x≠y"
          then obtain y where y:"y∈X""⟨x,y⟩∈r" "x≠y" by auto
          with x have "x∈IntervalX(X,r,b,y)" unfolding IntervalX_def Interval_def
            using ‹x∈X› by auto moreover
          have "⟨b,y⟩∈r" using y(2) x(1) assms(1) unfolding IsLinOrder_def trans_def by fast
          moreover have "b≠y" using y(2,3) x(1) assms(1) unfolding IsLinOrder_def antisym_def by fast
          ultimately
          have "(∃z∈A-{b,y}. ⟨b,z⟩∈r∧⟨z,y⟩∈r)" using assms(2) unfolding IsWeaklyDenseSub_def
            using y(1) b(1) by auto
          then obtain z where "z∈A""⟨b,z⟩∈r""b≠z" by auto
          then have "z∈A∩V" using b(2) unfolding RightRayX_def using assms(3) by auto
          then have "z∈A∩U" using V(2) by auto
          then have "A∩U≠0" by auto
        }
        moreover
        {
          assume R:"∀y∈X. ⟨x,y⟩∈r⟶x=y"
          {
            fix y assume "y∈RightRayX(X,r,b)"
            then have y:"⟨b,y⟩∈r" "y∈X-{b}" unfolding RightRayX_def by auto
            {
              assume A:"y≠x"
              then have "⟨x,y⟩∉r" using R y(2) by auto
              then have "⟨y,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
                using ‹x∈X› y(2) by auto
              with A y have "y∈IntervalX(X,r,b,x)" unfolding IntervalX_def Interval_def
                by auto
              then have "False" using B by auto
            }
            then have "y=x" by auto
          }
          then have "RightRayX(X,r,b)={x}" using V(3) b(2) by blast
          moreover
          {
            fix t assume T:"t∈X"
            {
              assume "t=x"
              then have "⟨t,x⟩∈r" using assms(1) unfolding IsLinOrder_def
                using Order_ZF_1_L1 T by auto
            }
            moreover
            {
              assume "t≠x"
              then have "⟨x,t⟩∉r" using R T by auto
              then have "⟨t,x⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
                using T ‹x∈X› by auto
            }
            ultimately have "⟨t,x⟩∈r" by auto
          }
          with ‹x∈X› have HM:"HasAmaximum(r,X)" unfolding HasAmaximum_def by auto
          then have "Maximum(r,X)∈X""∀t∈X. ⟨t,Maximum(r,X)⟩∈r" using Order_ZF_4_L3 assms(1) unfolding IsLinOrder_def
            by auto
          with R ‹x∈X› have xm:"x=Maximum(r,X)" by auto
          moreover note b(2)
          ultimately have "V={Maximum(r,X)}" by auto
          then have "{Maximum(r,X)}∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
            V(1) by auto
          with HM have "Maximum(r,X)∈A" using assms(6) by auto
          with xm have "x∈A" by auto
          with V(2,3) have "A∩U≠0" by auto
        }
        ultimately have "A∩U≠0" by auto
      }
      moreover
      {
        assume "IntervalX(X, r, b, x) ≠ 0"
        with disj have "∃z∈A-{b,x}. ⟨b,z⟩∈r∧⟨z,x⟩∈r" by auto
        then obtain z where "z∈A""z≠b""⟨b,z⟩∈r" by auto
        then have "z∈A""z∈RightRayX(X,r,b)" unfolding RightRayX_def using assms(3) by auto
        then have "z∈A∩U" using V(2) b(2) by auto
        then have "A∩U≠0" by auto
      }
      ultimately have "A∩U≠0" by auto
    }
    moreover
    {
      assume "V∈{LeftRayX(X, r, b) . b ∈ X}"
      then obtain b where b:"b∈X""V=LeftRayX(X, r, b)" by auto
      with V(3) have x:"⟨x,b⟩∈r" "b≠x" unfolding LeftRayX_def by auto moreover
      note b(1) moreover
      have "U⊆⋃(OrdTopology X r)" using ass(2) by auto
      then have "U⊆X" using union_ordtopology[OF assms(1,4)] by auto
      then have "x∈X" using ass(1) by auto moreover
      note assms(2) ultimately
      have disj:"(∃z∈A-{b,x}. ⟨x,z⟩∈r∧⟨z,b⟩∈r)∨ IntervalX(X, r, x, b) = 0" unfolding IsWeaklyDenseSub_def by auto
      {
        assume B:"IntervalX(X, r, x, b) = 0"
        {
          assume "∃y∈X. ⟨y,x⟩∈r ∧ x≠y"
          then obtain y where y:"y∈X""⟨y,x⟩∈r" "x≠y" by auto
          with x have "x∈IntervalX(X,r,y,b)" unfolding IntervalX_def Interval_def
            using ‹x∈X› by auto moreover
          have "⟨y,b⟩∈r" using y(2) x(1) assms(1) unfolding IsLinOrder_def trans_def by fast
          moreover have "b≠y" using y(2,3) x(1) assms(1) unfolding IsLinOrder_def antisym_def by fast
          ultimately
          have "(∃z∈A-{b,y}. ⟨y,z⟩∈r∧⟨z,b⟩∈r)" using assms(2) unfolding IsWeaklyDenseSub_def
            using y(1) b(1) by auto
          then obtain z where "z∈A""⟨z,b⟩∈r""b≠z" by auto
          then have "z∈A∩V" using b(2) unfolding LeftRayX_def using assms(3) by auto
          then have "z∈A∩U" using V(2) by auto
          then have "A∩U≠0" by auto
        }
        moreover
        {
          assume R:"∀y∈X. ⟨y,x⟩∈r⟶x=y"
          {
            fix y assume "y∈LeftRayX(X,r,b)"
            then have y:"⟨y,b⟩∈r" "y∈X-{b}" unfolding LeftRayX_def by auto
            {
              assume A:"y≠x"
              then have "⟨y,x⟩∉r" using R y(2) by auto
              then have "⟨x,y⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
                using ‹x∈X› y(2) by auto
              with A y have "y∈IntervalX(X,r,x,b)" unfolding IntervalX_def Interval_def
                by auto
              then have "False" using B by auto
            }
            then have "y=x" by auto
          }
          then have "LeftRayX(X,r,b)={x}" using V(3) b(2) by blast
          moreover
          {
            fix t assume T:"t∈X"
            {
              assume "t=x"
              then have "⟨x,t⟩∈r" using assms(1) unfolding IsLinOrder_def
                using Order_ZF_1_L1 T by auto
            }
            moreover
            {
              assume "t≠x"
              then have "⟨t,x⟩∉r" using R T by auto
              then have "⟨x,t⟩∈r" using assms(1) unfolding IsLinOrder_def IsTotal_def
                using T ‹x∈X› by auto
            }
            ultimately have "⟨x,t⟩∈r" by auto
          }
          with ‹x∈X› have HM:"HasAminimum(r,X)" unfolding HasAminimum_def by auto
          then have "Minimum(r,X)∈X""∀t∈X. ⟨Minimum(r,X),t⟩∈r" using Order_ZF_4_L4 assms(1) unfolding IsLinOrder_def
            by auto
          with R ‹x∈X› have xm:"x=Minimum(r,X)" by auto
          moreover note b(2)
          ultimately have "V={Minimum(r,X)}" by auto
          then have "{Minimum(r,X)}∈(OrdTopology X r)" using base_sets_open[OF Ordtopology_is_a_topology(2)[OF assms(1)]]
            V(1) by auto
          with HM have "Minimum(r,X)∈A" using assms(5) by auto
          with xm have "x∈A" by auto
          with V(2,3) have "A∩U≠0" by auto
        }
        ultimately have "A∩U≠0" by auto
      }
      moreover
      {
        assume "IntervalX(X, r, x, b) ≠ 0"
        with disj have "∃z∈A-{b,x}. ⟨x,z⟩∈r∧⟨z,b⟩∈r" by auto
        then obtain z where "z∈A""z≠b""⟨z,b⟩∈r" by auto
        then have "z∈A""z∈LeftRayX(X,r,b)" unfolding LeftRayX_def using assms(3) by auto
        then have "z∈A∩U" using V(2) b(2) by auto
        then have "A∩U≠0" by auto
      }
      ultimately have "A∩U≠0" by auto
    }
    ultimately have "A∩U≠0" by auto
  }
  then have "∀U∈(OrdTopology X r). x∈U ⟶ U∩A≠0" by auto
  moreover note ‹x∈X› moreover
  note assms(3) topology0.inter_neigh_cl[OF topology0_ordtopology[OF assms(1)]]
  union_ordtopology[OF assms(1,4)] ultimately have "x∈Closure(A,OrdTopology X r)"
    by auto
  }
  then have "X⊆Closure(A,OrdTopology X r)" by auto
  with topology0.Top_3_L11(1)[OF topology0_ordtopology[OF assms(1)]]
    assms(3) union_ordtopology[OF assms(1,4)] show ?thesis by auto
qed

text‹The conclusion is that an order topology is $\kappa$-separable
iff there is a set $A$ with cardinality strictly less than $\kappa$
which is weakly-dense in $X$.›

theorem separable_imp_wdense:
  assumes "(OrdTopology X r){is separable of cardinal}Q" "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X"
    "IsLinOrder(X,r)"
  shows "∃A∈Pow(X). A≺Q ∧ (A{is weakly dense in}X{with respect to}r)"
proof-
  from assms obtain U where "U∈Pow(⋃(OrdTopology X r))" "Closure(U,OrdTopology X r)=⋃(OrdTopology X r)" "U≺Q"
    unfolding IsSeparableOfCard_def by auto
  then have "U∈Pow(X)" "Closure(U,OrdTopology X r)=X" "U≺Q" using union_ordtopology[OF assms(3,2)]
    by auto
  with dense_top_imp_Wdense_ord[OF assms(3) _ _ assms(2)] show ?thesis by auto
qed

theorem wdense_imp_separable:
  assumes "∃x y. x ≠ y ∧ x ∈ X ∧ y ∈ X" "(A{is weakly dense in}X{with respect to}r)"
    "IsLinOrder(X,r)" "A≺Q" "InfCard(Q)" "A⊆X"
  shows "(OrdTopology X r){is separable of cardinal}Q"
proof-
  {
    assume Hmin:"HasAmaximum(r,X)"
    then have MaxX:"Maximum(r,X)∈X" using Order_ZF_4_L3(1) assms(3) unfolding IsLinOrder_def
      by auto
    {
      assume HMax:"HasAminimum(r,X)"
      then have MinX:"Minimum(r,X)∈X" using Order_ZF_4_L4(1) assms(3) unfolding IsLinOrder_def
        by auto
      let ?A="A ∪{Maximum(r,X),Minimum(r,X)}"
      have "Finite({Maximum(r,X),Minimum(r,X)})" by auto
      then have "{Maximum(r,X),Minimum(r,X)}≺nat" using n_lesspoll_nat
        unfolding Finite_def using eq_lesspoll_trans by auto
      moreover
      from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
        using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
        using Card_is_Ord[of "Q"] by auto
      ultimately have "{Maximum(r,X),Minimum(r,X)}≺Q" using lesspoll_trans by auto
      with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
        by auto
      have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
        IsWeaklyDenseSub_def by auto
      from MaxX MinX assms(6) have S:"?A⊆X" by auto
      then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
        [OF assms(3) WeakDense _ assms(1)] by auto
      then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
        S C by auto
    }
    moreover
    {
      assume nmin:"¬HasAminimum(r,X)"
       let ?A="A ∪{Maximum(r,X)}"
      have "Finite({Maximum(r,X)})" by auto
      then have "{Maximum(r,X)}≺nat" using n_lesspoll_nat
        unfolding Finite_def using eq_lesspoll_trans by auto
      moreover
      from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
        using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
        using Card_is_Ord[of "Q"] by auto
      ultimately have "{Maximum(r,X)}≺Q" using lesspoll_trans by auto
      with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
        by auto
      have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
        IsWeaklyDenseSub_def by auto
      from MaxX assms(6) have S:"?A⊆X" by auto
      then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
        [OF assms(3) WeakDense _ assms(1)] nmin by auto
      then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
        S C by auto
    }
    ultimately have ?thesis by auto
  }
  moreover
  {
    assume nmax:"¬HasAmaximum(r,X)"
    {
      assume HMin:"HasAminimum(r,X)"
      then have MinX:"Minimum(r,X)∈X" using Order_ZF_4_L4(1) assms(3) unfolding IsLinOrder_def
        by auto
      let ?A="A ∪{Minimum(r,X)}"
      have "Finite({Minimum(r,X)})" by auto
      then have "{Minimum(r,X)}≺nat" using n_lesspoll_nat
        unfolding Finite_def using eq_lesspoll_trans by auto
      moreover
      from assms(5) have "nat≺Q∨nat=Q" unfolding InfCard_def
        using lt_Card_imp_lesspoll[of "Q""nat"] unfolding lt_def succ_def
        using Card_is_Ord[of "Q"] by auto
      ultimately have "{Minimum(r,X)}≺Q" using lesspoll_trans by auto
      with assms(4,5) have C:"?A≺Q" using less_less_imp_un_less
        by auto
      have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
        IsWeaklyDenseSub_def by auto
      from MinX assms(6) have S:"?A⊆X" by auto
      then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
        [OF assms(3) WeakDense _ assms(1)] nmax by auto
      then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
        S C by auto
    }
    moreover
    {
      assume nmin:"¬HasAminimum(r,X)"
      let ?A="A"
      from assms(4,5) have C:"?A≺Q" by auto
      have WeakDense:"?A{is weakly dense in}X{with respect to}r" using assms(2) unfolding
        IsWeaklyDenseSub_def by auto
      from assms(6) have S:"?A⊆X" by auto
      then have "Closure(?A,OrdTopology X r)=X" using Wdense_ord_imp_dense_top
        [OF assms(3) WeakDense _ assms(1)] nmin nmax by auto
      then have ?thesis unfolding IsSeparableOfCard_def using union_ordtopology[OF assms(3,1)]
        S C by auto
    }
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed


end