--- a/src/ODC.agda	Fri Apr 01 20:15:08 2022 +0900
+++ b/src/ODC.agda	Sat Apr 02 08:32:01 2022 +0900
@@ -180,6 +180,7 @@
      ind nomx x prev with Oprev-p x
      ... | yes op with ∋-p A (* x)
      ... | no ¬Ax = record  { B = ZChain.B zc1 ; B⊆A =  ZChain.B⊆A  zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = z04 } where
+          -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
           px = Oprev.oprev op
           zc1 : ZChain A px _<_
           zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
@@ -190,31 +191,37 @@
           ... | tri> ¬a ¬b c with  osuc-≡< s<x
           ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )  
           ... | case2 lt = ⊥-elim (¬a lt )
-     ... | yes ax = z06 where
+     ... | yes ax = z06 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
           zc1 : ZChain A px _<_
           zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           z06 : ZChain A x _<_
           z06 with is-o∅ (& (Gtx ax))
-          ... | yes nogt = ⊥-elim (no-maximum nomx x x-is-maximal ) where
+          ... | yes nogt = ⊥-elim (no-maximum nomx x x-is-maximal ) where -- no larger element, so it is maximal
               x-is-maximal :  (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
               x-is-maximal m am  = ⟪ subst (λ k → odef A k) &iso ax ,  ¬x<m  ⟫ where
                  ¬x<m :  ¬ (* x < * m)
                  ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
-          ... | no not = record { B = Bx
-              ; B⊆A = {!!} ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
-                 B = ZChain.B (prev px (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc)) 
+          ... | no not = record { B = Bx     --  we have larger element, let's create ZChain
+              ; B⊆A = B⊆A ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
+                 B = ZChain.B zc1 
                  Bx : HOD
-                 Bx = record { od = record { def = λ y → (x ≡ y) ∨ odef B x } ; odmax = {!!} ; <odmax = {!!}  } 
+                 Bx = record { od = record { def = λ y → (x ≡ y) ∨ odef B y } ; odmax = & A ; <odmax = {!!}  } 
+                 B⊆A : Bx ⊆ A
+                 B⊆A = record { incl = λ {y} by → z07 y by  } where
+                     z07 : (y : HOD) → Bx ∋ y → A ∋ y
+                     z07 y (case1 x=y) = subst (λ k → odef A k ) (trans &iso x=y) ax
+                     z07 y (case2 by) = incl (ZChain.B⊆A zc1 ) by
                  m = minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
-     ind nomx x prev | no ¬ox with trio< (& A) x
-     ... | tri< a ¬b ¬c = {!!} where
+     ind nomx x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
+     ... | tri< a ¬b ¬c = record { B = ZChain.B zc1
+              ; B⊆A = ZChain.B⊆A zc1 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = {!!} } where
           zc1 : ZChain A (& A) _<_
           zc1 = prev (& A) a 
-     ... | tri≈ ¬a b ¬c = record { B = ?
-              ; B⊆A = ? ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
-          zc1 : ZChain A {!!} _<_
-          zc1 = prev {!!} {!!}
+     ... | tri≈ ¬a b ¬c = record { B = B
+              ; B⊆A = {!!} ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} } where
+          B : HOD
+          B = record { od = record { def = λ y → (y<x : y o< x ) → odef (ZChain.B (prev y y<x)) y } ; odmax = & A ; <odmax = {!!} } 
      ... | tri> ¬a ¬b c = {!!}
      zorn00 : Maximal A _<_
      zorn00 with is-o∅ ( & HasMaximal )