--- a/ordinal-definable.agda	Mon Jun 10 09:35:14 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 10 09:50:44 2019 +0900
@@ -45,16 +45,19 @@
 od∅ : {n : Level} → OD {n} 
 od∅ {n} = record { def = λ _ → Lift n ⊥ }
 
--- OD can be iso to a subset of Ordinal
+
 postulate      
+  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
   od→ord : {n : Level} → OD {n} → Ordinal {n}
   ord→od : {n : Level} → Ordinal {n} → OD {n} 
   c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
   oiso   : {n : Level} {x : OD {n}}      → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+  -- supermum as Replacement Axiom
   sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-o< : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
+  -- a property of supermum required in Power Set Axiom
   sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
@@ -340,8 +343,14 @@
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
-         --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
+         ---
+         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
+         --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
+         --
+         --  if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 
+         --    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
+         --
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
          power→ A t P∋t {x} t∋x = proj1 lemma-s where
               minsup :  OD
@@ -352,7 +361,10 @@
               lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso  )
               lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl
               lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst (o<→c< lt) oiso refl ) t∋x
-              -- = {!!} -- transitive {!!} t∋x
+         -- 
+         -- 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 : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A  = def-subst {suc n} {_} {_} {Power A} {od→ord t}
                   ( o<→c< {suc n} {od→ord (ZFSubset A (ord→od (od→ord t)) )} {sup-o (λ x → od→ord (ZFSubset A (ord→od x)))}