--- a/src/Tychonoff.agda	Sun Jan 22 20:15:15 2023 +0900
+++ b/src/Tychonoff.agda	Sun Jan 22 22:41:13 2023 +0900
@@ -189,14 +189,22 @@
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
          Pf = ?
-         neip : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TP (& p) ? 
-         neip = ?
-         neiq : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TQ (& q) ? 
-         neiq = ?
          pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F 
          pq⊆F = ?
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F 
-         isL {v} npq {x} fx = ?
+         isL {v} npq {x} fx = filter2 F ? ? ? where
+             neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
+             neip = ?
+             neiq : {q : Ordinal } → ( bq : BaseQ P TQ q ) → * q ⊆ filter F 
+             neiq = ?
+             bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
+             bpq = Neighbor.ou npq (Neighbor.ux npq)
+             pqb : Subbase (pbase TP TQ) (Base.b bpq )
+             pqb = Base.sb bpq 
+             base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆ filter F
+             base⊆F (gi (case1 px)) bx = ?
+             base⊆F (gi (case2 qx)) bx = ?
+             base⊆F (g∩ b1 b2) bx = filter1 F ? ? ?