--- a/src/ODC.agda	Tue Mar 22 15:40:57 2022 +0900
+++ b/src/ODC.agda	Wed Mar 23 16:42:42 2022 +0900
@@ -40,7 +40,7 @@
   minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
   -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
-  -- minimality (may proved by ε-induction with LEM)
+  -- minimality (proved by ε-induction with LEM)
   minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
 
 
@@ -111,7 +111,7 @@
       sup : HOD
       A∋maximal : A ∋ sup
       tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
-      x≤sup : (x : HOD) → (b : B ∋ x ) → (x ≡ sup ) ∨ (x < sup )
+      x≤sup : (x : HOD) → B ∋ x → (x ≡ sup ) ∨ (x < sup )
 
 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
@@ -119,35 +119,38 @@
       A∋maximal : HOD
       ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x
 
-record ZChain ( A : HOD ) (x : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
+record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      NOMAX : HOD
-      Chain : HOD
-      nomax : (y m : Ordinal) → odef NOMAX y → y o< x → ¬ ( * y < * m )
-      chain : (y : Ordinal) → odef Chain y → & NOMAX ≡ o∅  → SUP A (* y) _<_
+      B : HOD
+      B⊆A : B ⊆ A 
+      tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
+      fb : {x : HOD } → A ∋ x  → HOD
+      B∋fb : (x : HOD ) → (ax : A ∋ x)  → B ∋ fb ax
+      ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< y → sup < fb as
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B  _<_  )
     → Maximal A _<_ 
-Zorn-lemma {A} {_<_} 0<A SUP = zorn01 (TransFinite ind (& A)) where
-     HasGreater : Ordinal → HOD
-     HasGreater m = record { od = record { def = λ x → odef A x ∧ (* m < * x) } ; odmax = & A ; <odmax = {!!} }
-     zorn01 : ZChain A (& A) _<_ → Maximal A _<_
-     zorn01 zc with is-o∅ ( & (ZChain.NOMAX zc) )
-     ... | yes _ = {!!}
-     ... | no not = record { maximal = minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}
-         ; ¬maximal<x = λ x lt m<x → ZChain.nomax zc {!!} {!!} (x∋minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ) {!!} {!!}  }
+Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
+     HasMaximal : HOD
+     HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
+     ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
+     ZChain→¬SUP z sp = {!!}
      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
      ind x prev with Oprev-p x
-     ... | yes ox with is-o∅ (& (HasGreater x))
-     ... | yes _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
-     ... | no _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
+     ... | yes _ = {!!}
      ind x prev | no ¬ox with trio< (& A) x
      ... | tri< a ¬b ¬c = {!!}
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}
+     zorn00 : Maximal A _<_
+     zorn00 with is-o∅ ( & HasMaximal )
+     ... | no not = record { maximal = minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}; ¬maximal<x  = {!!} }
+     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP (ZChain.B (z (& A))) (ZChain.B⊆A (z (& A))) ) ) where
+         z : (x : Ordinal) → ZChain A x _<_ 
+         z = TransFinite ind 
 
 open import zfc