--- a/OD.agda	Sun May 10 09:25:18 2020 +0900
+++ b/OD.agda	Sun Jun 07 20:29:12 2020 +0900
@@ -246,7 +246,7 @@
     ; infinite = infinite
     ; isZF = isZF 
  } where
-    ZFSet = OD 
+    ZFSet = OD             -- is less than Ords because of maxod
     Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
@@ -260,7 +260,7 @@
     Power : OD  → OD 
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- ｛_｝ : ZFSet → ZFSet
-    -- ｛ x ｝ = ( x ,  x )
+    -- ｛ x ｝ = ( x ,  x )     -- it works but we don't use 
 
     data infinite-d  : ( x : Ordinal  ) → Set n where
         iφ :  infinite-d o∅