--- a/src/zorn.agda	Sat Apr 16 11:51:43 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 12:10:09 2022 +0900
@@ -392,9 +392,15 @@
      ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
      ... | no ¬Ax = {!!} where
      ... | yes ax = {!!}
-     ... | no not = {!!} where
      zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
      zorn03 x = TransFinite ind  x
+     zorn07 : (x : HOD) → (ax : A ∋ x ) → OSup> A (d→∋ A ax) ∨ Maximal A ∨ InFiniteIChain A (d→∋ A ax)
+     zorn07 x = ε-induction (λ {x} prev ax →  Zorn-lemma-3case 0<A PO (me {A} {x}  ax ) ) x
+     zorn05 : Maximal A 
+     zorn05 with zorn07 A {!!}
+     ... | case1 chain = {!!}
+     ... | case2 (case1 m) = m
+     ... | case2 (case2 chain) = {!!}
      zorn04 : Maximal A 
      zorn04 with zorn03 (& A)
      ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.max chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )