--- a/LEMC.agda	Sat May 09 16:41:40 2020 +0900
+++ b/LEMC.agda	Sat May 09 17:35:56 2020 +0900
@@ -84,16 +84,32 @@
                             eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
-         minimal-choice : (X : OD ) → ¬ (X == od∅) → choiced X
-         minimal-choice X ne = choice-func {!!} ne
+         record Minimal (x : OD)  : Set (suc n) where
+           field
+               min : OD
+               x∋min :  ¬ (x == od∅ ) → x ∋ min 
+               min-empty :  ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+         open Minimal
+         induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x
+         induction {x} prev = record {
+                  min = {!!}
+               ;  x∋min = {!!}
+               ;  min-empty = {!!}
+            } where
+             c1 : OD
+             c1 = a-choice (choice-func x {!!} ) 
+             c2 : OD
+             c2 with p∨¬p ( (y : OD ) →  def c1 (od→ord y) ∧ (def x (od→ord  y)))  
+             c2 | case1 _ = c1
+             c2 | case2 No =  {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y  } ) {!!}
+         Min1 : (x : OD) → Minimal x 
+         Min1 x = (ε-induction {λ y → Minimal y  } induction x ) 
          minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
-         minimal x not = a-choice (minimal-choice x not ) 
-         -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+         minimal x not = min (Min1 x) 
          x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = is-in (minimal-choice x ne )
-         -- minimality (may proved by ε-induction )
+         x∋minimal x ne = x∋min (Min1 x) ne
          minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
-         minimal-1 x ne y = {!!} 
+         minimal-1 x ne y = min-empty (Min1 x) ne y