# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592212548 -32400
# Node ID 42f89e5efb00569c5edce3ea795853e91386dc32
# Parent  822b50091a2665078fe320ae7299a5fd50c976a9
if Filter contains L, prime filter is ultra

diff -r 822b50091a26 -r 42f89e5efb00 filter.agda
--- a/filter.agda	Mon Jun 15 09:53:18 2020 +0900
+++ b/filter.agda	Mon Jun 15 18:15:48 2020 +0900
@@ -104,8 +104,20 @@
 --  if Filter contains L, prime filter is ultra
 --
 
-filter-lemma2 :  {L : OD} → (P : Filter L)  → prime-filter P → ultra-filter P
-filter-lemma2 {L} P prime  = {!!}
+filter-lemma2 :  {L : OD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
+filter-lemma2 {L} P f∋L prime = record {
+         proper = prime-filter.proper prime
+       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
+   } where
+        open _==_
+        p+1-p=1 : {p : OD} → p ⊆ L → L == (p ∪ (L ＼ p)) 
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (def p x)
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x  )) 
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
+        lemma : (p : OD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
+        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
 generated-filter {L} P p = {!!}