--- a/Ordinals.agda	Thu Aug 08 17:32:21 2019 +0900
+++ b/Ordinals.agda	Fri Aug 09 16:54:30 2019 +0900
@@ -13,17 +13,19 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-
-
-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set n where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
    field
      Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
      OTri : Trichotomous {n} _≡_  _o<_ 
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
+     TransFinite : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
 
-record Ordinals {n : Level} : Set (suc n) where
+
+record Ordinals {n : Level} : Set (suc (suc n)) where
    field
      ord : Set n
      o∅ : ord