--- a/src/filter.agda	Thu Mar 17 15:36:24 2022 +0900
+++ b/src/filter.agda	Thu Mar 17 16:40:54 2022 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+
 open import Level
 open import Ordinals
 module filter {n : Level } (O : Ordinals {n})   where
@@ -59,7 +61,7 @@
 open _⊆_
 
 ∈-filter : {L p : HOD} → (F : Filter L ) → filter F ∋ p → L ∋ p 
-∈-filter {L} {p} F lt = {!!} -- power→⊆ L p ( incl ? lt )
+∈-filter {L} {p} F lt = incl ( f⊆L F) lt 
 
 ∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
@@ -67,6 +69,12 @@
 ∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
 
+∪-lemma3 : {L P p q : HOD } → L ⊆ Power P → L ∋ (p ∪ q)  → L ∋ p
+∪-lemma3 = {!!}
+
+∪-lemma4 : {L P p q : HOD } →  L ⊆ Power P →  L ∋ (p ∪ q)  → L ∋ q
+∪-lemma4 = {!!}
+
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
@@ -83,8 +91,8 @@
        ; prime = lemma3
     } where
   lemma3 : {p q : HOD} → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
-  lemma3 {p} {q} lt with ultra-filter.ultra u {!!} -- (∪-lemma1 (∈-filter P lt) )
-  ... | case1 p∈P  = case1 p∈P
+  lemma3 {p} {q} lt with ultra-filter.ultra u (∈-filter F lt) 
+  ... | case1 p∈P  = case1 {!!} -- (∪-lemma3 (ultra-filter.L⊆PP u) ? ) --  : OD.def (od (filter F)) (& p)
   ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (L ＼ p)} {!!} lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
     lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
@@ -95,7 +103,7 @@
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma6 = filter2 F lt ¬p∈P
+    lemma6 = {!!} -- filter2 F lt ¬p∈P
     lemma7 : filter F ∋ (q ∩ (L ＼ p))
     lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) {!!}
     lemma8 : (q ∩ (L ＼ p)) ⊆ q