--- a/HOD.agda	Mon Jul 15 18:26:56 2019 +0900
+++ b/HOD.agda	Mon Jul 15 19:09:57 2019 +0900
@@ -217,19 +217,6 @@
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→
 
-OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
-OrdSubset {n} A x = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-  lemma1 :  {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y
-  lemma1 {y} s with trio< A x
-  lemma1 {y} s | tri< a ¬b ¬c = proj1 s
-  lemma1 {y} s | tri≈ ¬a refl ¬c = proj1 s
-  lemma1 {y} s | tri> ¬a ¬b c = proj2 s
-  lemma2 : {y : Ordinal} → def (Ord (minα A x)) y → def (ZFSubset (Ord A) (Ord x)) y
-  lemma2 {y} lt with trio< A x
-  lemma2 {y} lt | tri< a ¬b ¬c = record { proj1 = lt ; proj2 = ordtrans lt a }
-  lemma2 {y} lt | tri≈ ¬a refl ¬c = record { proj1 = lt ; proj2 = lt }
-  lemma2 {y} lt | tri> ¬a ¬b c = record { proj1 = ordtrans lt c ; proj2 = lt }
-
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
 -- L (Φ 0) = Φ
@@ -244,9 +231,6 @@
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
-omega : { n : Level } → Ordinal {n}
-omega = record { lv = Suc Zero ; ord = Φ 1 }
-
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -487,14 +471,10 @@
                     ≡ od→ord (Union (x , (x , x)))
                lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
 
-         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set
-         -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
-         record Choice (z : OD {suc n}) : Set (suc (suc n)) where
-             field
-                 u : {x : OD {suc n}} ( x∈z  : x ∈ z ) → OD {suc n}
-                 t : {x : OD {suc n}} ( x∈z  : x ∈ z ) → (x : OD {suc n} ) → OD {suc n}
-                 choice : { x : OD {suc n} } → ( x∈z  : x ∈ z ) → ( u x∈z ∩ x) == ｛ t x∈z x ｝
-         -- choice : {x :  OD {suc n}} ( x ∈ z  → ¬ ( x ≈ ∅ ) ) →
-         -- axiom-of-choice : { X : OD } → ( ¬x∅ : ¬ ( X == od∅ ) ) → { A : OD } → (A∈X : A ∈ X ) →  choice ¬x∅ A∈X ∈ A 
-         -- axiom-of-choice {X} nx {A} lt = ¬∅=→∅∈ {!!}
+         -- Axiom of choice ( is equivalent to existence of minimul )
+         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
+         choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
+         choice-func X {x} not X∋x = minimul x not
+         choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
+         choice X {A} X∋A not = x∋minimul A not