--- a/src/Tychonoff.agda	Fri Mar 03 16:33:56 2023 +0900
+++ b/src/Tychonoff.agda	Fri Mar 03 19:44:29 2023 +0900
@@ -206,9 +206,14 @@
         uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 
            ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12  )
 
+x⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → x ⊆ Cl TP x
+x⊆Clx {P} TP {x}  x<p {y} xy  = ⟪ x<p xy , (λ c csc x<c → x<c xy )  ⟫
+P⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → Cl TP x ⊆ P
+P⊆Clx {P} TP {x}  x<p {y} xy  = proj1 xy
+
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
-FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where
+FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
      --
      -- take closure of given filter elements
      --
@@ -219,22 +224,47 @@
      --
      -- it is set of closed set and has FIP ( F is proper )
      --
+     ufl08  : {z : Ordinal} → odef (Power P) (& (Cl TP (* z)))
+     ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw
+     ... | t = proj1 t
+     fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x
+     fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz )
+     F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x
+     F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where
+        ufl09 : * z ⊆ P
+        ufl09 {y} zy = f⊆L F az _ zy
+        ufl07 : odef (filter F) x
+        ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso))  ufl08  ) 
+            (subst (λ k → odef (filter F) k) (sym &iso) az) 
+            (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) ))
+     F∋sb  (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx))
+        (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) 
+            (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) )))   
      ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
-     ufl01 = ?
+     ufl01 {x} sb = ufl04  where
+        ufl04 : o∅ o< x 
+        ufl04 with trio< o∅ x 
+        ... | tri< a ¬b ¬c = a
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) (
+           begin 
+           x  ≡⟨ sym b ⟩
+           o∅ ≡⟨ sym ord-od∅ ⟩
+           & od∅  ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) ))  where open ≡-Reasoning
+        ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
      --
      -- so we have a limit
      --
      limit : Ordinal
-     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01  
+     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
      ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
-     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01  
+     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
      --
      -- 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 which is a closure
+     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} nei vx z pz = ?
+     pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = v⊆P ?
      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