--- a/src/Topology.agda	Fri Mar 03 21:31:12 2023 +0900
+++ b/src/Topology.agda	Sat Mar 04 10:26:35 2023 +0900
@@ -42,7 +42,7 @@
        OS⊆PL :  OS ⊆ Power L
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q      → OS ∋ (p ∩ q)
        o∪ : { P : HOD }  →  P ⊆ OS                → OS ∋ Union P
-       OS∋od∅ : OS ∋ od∅
+       OS∋od∅ : OS ∋ od∅ -- OS ∋ Union od∅ 
 --- we may add
 --     OS∋L   :  OS ∋ L
 -- closed Set
@@ -114,6 +114,12 @@
                 cc05 : odef (* (& (L ＼ * o))) x
                 cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) (sym *iso) A⊆L-o) 
 
+CS∋x→Clx=x : {L x : HOD} → (top : Topology L) → CS top ∋ x → Cl top x ≡ x 
+CS∋x→Clx=x {L} {x} top cx = ==→o≡ record { eq→ = cc10 ; eq← = cc11 } where
+    cc10 : {y : Ordinal} → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) → odef x y
+    cc10 {y} ⟪ Ly , cc ⟫ = subst (λ k → odef k y) *iso ( cc (& x) cx (λ {z} xz → subst (λ k → odef k z) (sym *iso) xz  ) )
+    cc11 : {y : Ordinal} → odef x y → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) 
+    cc11 {y} xy = ⟪ cs⊆L top cx xy , (λ c oc x⊆c → x⊆c xy ) ⟫
 
 -- Subbase P
 --   A set of countable intersection of P will be a base (x ix an element of the base)

--- a/src/Tychonoff.agda	Fri Mar 03 21:31:12 2023 +0900
+++ b/src/Tychonoff.agda	Sat Mar 04 10:26:35 2023 +0900
@@ -226,7 +226,6 @@
      ... | tri< a ¬b ¬c = a
      ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋P) )
      ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-
      --
      -- take closure of given filter elements
      --
@@ -278,14 +277,34 @@
      --
      -- Neigbor of limit ⊆ Filter
      --
-     ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅  -- because limit is in CF 
-     ufl03 {f} {v} ff nei fv=0 = ?
-     pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
-     pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = ?
+     -- if odef (* X) x, Cl TP x contains limit (ufl02)
+     -- in (nei : Neighbor TP limit v) , there is an open Set u which contains the limit
+     -- F contains u or P ＼ u because F is ultra
+     --   if F ∋ u, then F ∋ v from u ⊆ v which is a propetery of Neighbor
+     --   if F ∋ P ＼ u, it is a closed set (Cl (P ＼ u) ≡ P ＼ u) and it does not contains the limit 
+     --      this contradicts ufl02
+     pp :  {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei))
+     pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz 
+        = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) 
      ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 
-     ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
-     ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
-     ... | case2 nfv = ? -- will contradicts ufl03
+     ufl00 {v} nei {x} vx with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei ))
+     ... | case1 fu = ? where -- Neighbor.u⊆v nei ? where
+         -- subst (λ k → odef (filter F) k) &iso ( filter1 F ? ? ? ) where
+         px : Power P ∋ * x
+         px z xz = Neighbor.v⊆P nei ?
+     ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where
+         u = * (Neighbor.u nei)
+         P\u : HOD
+         P\u = P ＼ u
+         P\u∋limit : odef P\u limit
+         P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where
+             ufl04 : & P\u ≡ & (Cl TP (* (& P\u)))
+             ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) 
+                (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) )))))
+             ufl03 : odef CF (& P\u )
+             ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 }
+         ¬P\u∋limit : ¬ odef P\u limit
+         ¬P\u∋limit ⟪ Pl , nul ⟫ = nul ( Neighbor.ux nei )
 
 -- product topology of compact topology is compact