--- a/src/OD.agda	Sun Jul 10 10:51:30 2022 +0900
+++ b/src/OD.agda	Sun Jul 10 16:22:46 2022 +0900
@@ -223,6 +223,12 @@
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
 
+∈∅< : { x : HOD  } {y : Ordinal } → odef x y → o∅  o< (& x)
+∈∅<  {x} {y} d with trio< o∅ (& x)
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( ∅< {x} {* y} (subst (λ k → odef x k ) (sym &iso) d )  ( ≡o∅→=od∅ (sym b) ) )
+... | tri> ¬a ¬b c = ⊥-elim (  ¬x<0 c  )
+
 ∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
 ∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )
 
@@ -248,7 +254,7 @@
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
--- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
+-- another possible restriction. We require no minimality on odmax, so it may arbitrary larger.
 odmax<&  : { x y : HOD } → x ∋ y →  Set n
 odmax<& {x} {y} x∋y = odmax x o< & x
 

--- a/src/zorn.agda	Sun Jul 10 10:51:30 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 16:22:46 2022 +0900
@@ -263,12 +263,12 @@
       psup :  Ordinal → Ordinal 
       p≤z : (x : Ordinal ) →   odef A (psup x)
       chainf : (x : Ordinal) → HOD
-      is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x ) w 
+      is-chain : (x w : Ordinal) → odef (chainf x) w → Chain A f mf ay (psup x) w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = ZChain1.chainf (zc0 (& A)) z 
+   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x )  
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -515,17 +515,21 @@
             ... | no z<x  = ZChain1.p≤z (pzc z (o¬≤→< z<x)) z
             chainf1 : (z : Ordinal ) → HOD
             chainf1 z with o≤? x z
-            ... | yes _  = record { od = record { def = λ w → odef A w ∧ (odef UZ w ∨ FClosure A f spu w ) } ; odmax = & A ; <odmax = ? }
+            ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = ? }
             ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
             is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
             is-chain1 z w lt with o≤? x z
             ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
-            is-chain1 z w ⟪ aw , case1 uz ⟫   | yes _ = subst (λ k → Chain A f mf ay k w) ? uz02  where
-                uz02 : Chain A f mf ay (ZChain1.psup (pzc (UChain.u (proj2 uz)) (UChain.u<x (proj2 uz))) (UChain.u (proj2 uz))) w
-                uz02 = (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 uz))) _ _  (UChain.chain∋z (proj2 uz) ))
-            is-chain1 z w ⟪ aw , case2 uzfc ⟫ | yes _ = ch-is-sup ? ? is-sup uzfc where
-                0<s : ?
-                0<s = ?
+            is-chain1 z w ⟪ ax , ux ⟫ | yes _ with trio< o∅ spu
+            ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+            ... | tri≈ ¬a b ¬c = ch-init _ _ (sym b) ? where
+                sc0 : FClosure A f spu w
+                sc0 = ux
+            ... | tri< a ¬b ¬c = ch-is-sup 0<s aspu is-sup ux where
+                0<s : o∅ o< spu
+                0<s = a 
+                aspu : odef A spu
+                aspu = SUP.A∋maximal usup
                 is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay x1 w₁ → w₁ << & (SUP.sup usup)
                 is-sup = ?