--- a/src/filter.agda	Sat Apr 16 12:10:09 2022 +0900
+++ b/src/filter.agda	Sat Apr 16 12:20:08 2022 +0900
@@ -228,20 +228,24 @@
      F∋-p = incl U⊆F U∋-p 
      f0 : filter F ∋ od∅
      f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) )
- 
--- open import zorn 
+
+_⊆'_ : ( A B : HOD ) → Set n
+_⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
+
+import zorn 
+open zorn O _⊆'_
 
--- MaximumSubset : {L P : HOD} 
---        → o∅ o< & L →  o∅ o< & P → P ⊆ L
---        → IsPartialOrderSet P _⊆'_
---        → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
---        → Maximal P (_⊆'_)
--- MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆'_} 0<P PO SP
+MaximumSubset : {L P : HOD} 
+      → o∅ o< & L →  o∅ o< & P → P ⊆ L
+      → IsPartialOrderSet P 
+      → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B  → SUP P B  )
+      → Maximal P 
+MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma 0<P PO SP
 
--- MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
---        → (F : Filter LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter LP 
--- MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = {!!} where
---       mf01 : Maximal O P (_⊆'_ O)
---       mf01 = MaximumSubset O 0<L {!!}  {!!} {!!} {!!} 
+MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
+      → (F : Filter LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter LP 
+MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
+     mf01 : Maximal  P 
+     mf01 = MaximumSubset  0<L {!!}  {!!} {!!} {!!}