--- a/src/zorn.agda	Sat Apr 16 18:14:48 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 18:52:48 2022 +0900
@@ -345,15 +345,21 @@
         zc9 y cy with  ODC.∋-p O (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) (* y)
         ... | no not = ⊥-elim (not (subst (λ k → odef (IChainSet {A} (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) k ) (sym &iso) cy))
         ... | yes cy1  with is-o∅ (& (Nx y (proj1 cy) ))
-        ... | yes no-next = {!!} 
+        ... | yes no-next = ⊥-elim zc16 where
+             zc18 : IChainSup> A (d→∋ A (is-elm x)) → ⊥
+             zc18 ics = ¬A∋x→A≡od∅ (Nx y (proj1 cy) ) ⟪ {!!} , ? ⟫ no-next  
+             zc17 : IsFC A {& (elm x)} (d→∋ A (is-elm x)) (& (* y))
+             zc17 = record { icf = cy ; c-finite = λ icsup → zc18 icsup }
+             zc16 : ⊥
+             zc16 = ¬A∋x→A≡od∅ HG ⟪ subst (λ k → odef A k ) (sym &iso) (proj1 cy ) , zc17 ⟫ inifite 
         ... | no not = record { y = zc14 ; A∋y = IChainSup>.A∋y (proj2 zc12) ; y>x = zc15 } where
-                  zc13 = ODC.minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
-                  zc12 : odef A (& zc13 ) ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) (proj1 cy) )
-                  zc12 = ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
-                  zc14 : Ordinal
-                  zc14 = IChainSup>.y (proj2 zc12) 
-                  zc15 : * y < * ( IChainSup>.y (proj2 (ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq)))) )
-                  zc15 = IChainSup>.y>x (proj2 zc12)
+             zc13 = ODC.minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+             zc12 : odef A (& zc13 ) ∧ IChainSup> A (subst (λ k → odef A k) (sym &iso) (proj1 cy) )
+             zc12 = ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq ))
+             zc14 : Ordinal
+             zc14 = IChainSup>.y (proj2 zc12) 
+             zc15 : * y < * ( IChainSup>.y (proj2 (ODC.x∋minimal O (Nx y (proj1 cy)) (λ eq → not (=od∅→≡o∅ eq)))) )
+             zc15 = IChainSup>.y>x (proj2 zc12)
 
 all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
      → (( x : Element A) → OSup> A (d→∋ A (is-elm x) ))