--- a/src/Topology.agda	Sat Jan 21 13:16:27 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 18:30:23 2023 +0900
@@ -468,6 +468,15 @@
        P∋limit : odef P limit
        is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v)
 
+Neighbor→F : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x) 
+Neighbor→F {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = ? ; filter2 = ? } where
+    NF : HOD
+    NF = record { od = record { def = λ v → Neighbor TP x v } ; odmax = ? ; <odmax = ? }
+    NF⊆PP : NF ⊆ Power P
+    NF⊆PP = nf00 where
+       nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v
+       nf00 {v} nei y vy = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso)  (Neighbor.ou nei)) ?
+
 -- FIP is UFL
 
 -- filter Base
@@ -540,7 +549,10 @@
          (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)))
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
             {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CSX fip)
-     uf01 {X} CSX fp {x} xx = ?
+     uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp (λ x → x)
+         ( MaximumFilter.mf (maxf CSX fp) )
+         (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp))) 
+            record { u = ? ; ou = ? ; ux = ? ; v⊆P = ? ; o⊆u = ? } ?
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF