--- a/OD.agda	Tue Sep 17 09:29:27 2019 +0900
+++ b/OD.agda	Sun Sep 22 20:26:32 2019 +0900
@@ -361,6 +361,9 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
+-- minimal-2 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+-- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
+
 OD→ZF : ZF  
 OD→ZF   = record { 
     ZFSet = OD 
@@ -548,6 +551,16 @@
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 
+         ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x}
+         ord⊆power a x lt = power← (Ord a) x lemma where
+                lemma : {y : OD} → x ∋ y → Ord a ∋ y
+                lemma y<x with osuc-≡< lt
+                lemma y<x | case1 refl = c<→o< y<x
+                lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
+
+         -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
+         -- continuum-hyphotheis a x = ?
+
          --  assuming axiom of choice
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)