--- a/src/Tychonoff.agda	Fri Mar 03 12:55:34 2023 +0800
+++ b/src/Tychonoff.agda	Fri Mar 03 16:33:56 2023 +0900
@@ -139,10 +139,15 @@
               f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
                  → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
      --
-     -- it contains no empty sets
+     -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x )
      -- 
-     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
-     proper = ?
+     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅)
+     proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where
+          x≤0 : x o< osuc  o∅
+          x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u))
+          fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x
+          fp00 b y b<X (gi by ) = gi ( b<X by )
+          fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz)
      --
      -- then we have maximum ultra filter 
      --
@@ -172,6 +177,8 @@
      ... | case1 lt = lt -- odef (* x) y
      ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf CSX fp) uf11 ) where
         y = UFLP.limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) 
+        x⊆P : * x ⊆ P
+        x⊆P = cs⊆L TP (CSX (subst (λ k → odef (* X) k) (sym &iso) xx))
         uf10 : odef (P ＼ * x ) y
         uf10 = nlxy
         uf03 : Neighbor TP y (& (P ＼ * x ))
@@ -179,15 +186,22 @@
            ; ux = subst (λ k → odef k y) (sym *iso) uf10  
            ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
            ; u⊆v = λ x → x  } 
+        uf07 : * (& (* x , * x)) ⊆ * X 
+        uf07 {y} lt with subst (λ k → odef k y) *iso lt
+        ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
+        ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
         uf05 : odef (filter (MaximumFilter.mf (maxf CSX fp))) x
-        uf05 = MaximumFilter.F⊆mf (maxf CSX fp) record { b = & (* x , * x) 
-           ; b⊆X = ? ; sb = gi ?  ; u⊆P = ? ; x⊆u = λ x → x  }
+        uf05 = MaximumFilter.F⊆mf (maxf CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 
+           ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  ; u⊆P = x⊆P ; x⊆u = λ x → x  }
         uf06 : odef (filter (MaximumFilter.mf (maxf CSX fp))) (& (P ＼ * x ))
         uf06 = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) uf03 (subst (λ k → odef k y) (sym *iso) uf10) 
         uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
-        uf13 = ?
+        uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
+           uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y
+           uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy )
         uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x )))
-        uf12 z pz = ?
+        uf12 z pz with subst (λ k → odef k z) *iso pz
+        ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz
         uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅
         uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 
            ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12  )