--- a/src/zorn.agda	Sat Jul 16 00:03:47 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 00:22:46 2022 +0900
@@ -674,6 +674,7 @@
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=px (sym &iso)) 
                           (IsSup.x<sup b=sup (chain-mono zy) )  } ) 
      ... | no op = zc5 where
+
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
           psupf0 : (z : Ordinal) → Ordinal
@@ -683,6 +684,16 @@
           ... | tri> ¬a ¬b c = y
           pchain : HOD
           pchain = UnionCF A f mf ay psupf0 x
+
+          record UZChain  (z : Ordinal) : Set n where 
+            field
+              z<x : z o< x
+              uc : UChain A f mf ay (ZChain.supf (pzc z z<x)) x z
+
+          pchain' : HOD
+          pchain' = record { od = record { def = λ z → odef A z ∧ UZChain z } 
+             ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )