--- a/HOD.agda	Mon Jul 01 01:27:25 2019 +0900
+++ b/HOD.agda	Mon Jul 01 16:03:15 2019 +0900
@@ -345,28 +345,35 @@
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
          --
+         POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t)
+         POrd {A} {t} P∋t = o<→c< P∋t
          power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x with osuc-≡<  (sup-lb  P∋t)
-         ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) 
-         ... | case2 lt = otrans A (proj1 (lemma lt )) (c<→o< {suc n} {x} {t} t∋x) where
+         power→ A t P∋t {x} t∋x with osuc-≡<  (sup-lb  (POrd P∋t))
+         ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  where
+              Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
+              Ltx {n} {x} {t} lt = c<→o< lt
+         ... | case2 lt = otrans A (proj1 (lemma1 lt) )
+                   (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where
               minsup :  HOD
               minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
-              lemma : od→ord t o< od→ord minsup → minsup ∋ t
-              lemma lt = {!!}
+              Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
+              Ltx {n} {x} {t} lt = c<→o< lt
+              lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
+              lemma1 lt = ?
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
          -- 
          power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
-                 lemma refl lemma1 where
+                 lemma refl (lemma1 lemma-eq )where
               lemma-eq :  ZFSubset A t == t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {A} {z}
                     ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ lemma-eq ))
+              lemma1 : {n : Level } { A t : HOD {suc n}} → (eq : ZFSubset A t == t)  → od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
+              lemma1 {n} {A} {t} eq = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
               lemma = sup-o<   
          union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}