--- a/src/zorn.agda	Sun Jun 26 23:41:10 2022 +0900
+++ b/src/zorn.agda	Mon Jun 27 00:48:05 2022 +0900
@@ -386,7 +386,8 @@
      --
 
      ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
-     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
+     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = λ lt →
+        subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc _ f mf lt )) ) }
      init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
      init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
                      ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf  ; chain = ys ay f mf
@@ -396,12 +397,12 @@
                is-max : {a b : Ordinal} → odef (ys ay f mf) a →
                     b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
                     * a < * b → odef (ys ay f mf) b
-               is-max {a} {b} yca b≤x ab P a<b = ?
+               is-max {a} {b} yca b≤x ab (case1 prev) a<b = subst (λ k → FClosure A f y k ) (sym (HasPrev.x=fy prev )) ( fsuc (HasPrev.y prev) (HasPrev.ay prev) )
+               is-max {a} {b} yca b≤x ab (case2 sup) a<b with IsSup.x<sup sup (init ay)
+               ... | case1 y=b = subst ( λ k → FClosure A f y k )  y=b  (init ay)
+               ... | case2 y<b = ?
                initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
-               initial {i} (init ai) = case1 refl
-               initial .{f x} (fsuc x lt) = {!!}
-
-
+               initial lt = s≤fc _ f mf lt
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x