--- a/LEMC.agda	Sat May 09 09:40:18 2020 +0900
+++ b/LEMC.agda	Sat May 09 16:41:40 2020 +0900
@@ -84,4 +84,17 @@
                             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
+         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 )
+         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 )
+         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 = {!!} 
+
+
+