--- a/HOD.agda	Wed Jun 26 22:53:30 2019 +0900
+++ b/HOD.agda	Thu Jun 27 08:34:19 2019 +0900
@@ -22,6 +22,7 @@
 open import Data.Unit
 
 open Ordinal
+open _∧_
 
 record _==_ {n : Level} ( a b :  HOD {n} ) : Set n where
   field
@@ -42,6 +43,10 @@
 eq-trans : {n : Level} {  x y z :  HOD {n} } → x == y → y == z → x == z
 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
 
+⇔→== : {n : Level} {  x y :  HOD {suc n} } → ( {z : Ordinal {suc n}} → def x z ⇔  def y z) → x == y 
+eq→ ( ⇔→== {n} {x} {y}  eq ) {z} m = proj1 eq m 
+eq← ( ⇔→== {n} {x} {y}  eq ) {z} m = proj2 eq m 
+
 -- Ordinal in HOD ( and ZFSet )
 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
 Ord {n} a = record { def = λ y → y o< a ; otrans = lemma }  where
@@ -59,6 +64,7 @@
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
+  ==→o≡ : {n : Level} →  { x y : HOD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
   -- supermum as Replacement Axiom
@@ -194,8 +200,8 @@
 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
 ∅< {n} {x} {y} d eq | lift ()
        
--- ∅6 : {n : Level} →  { x : HOD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
--- ∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x
+∅6 : {n : Level} →  { x : HOD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
+∅6 {n} {x} x∋x = o<¬≡ refl ( c<→o< {suc n} {x} {x} x∋x )
 
 def-iso : {n : Level} {A B : HOD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
@@ -205,10 +211,6 @@
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
 
-open _∧_
-
-ord⇔ : {n : Level} →  ( x y : HOD {suc n} ) → ( {z : Ordinal {suc n} } → def x z ⇔ def y z ) → od→ord x ≡ od→ord y
-ord⇔ = {!!}
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
@@ -394,7 +396,15 @@
          infinity∅ : Ord omega  ∋ od∅ {suc n}
          infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl
          infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = {!!} where
+         infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
+              eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
+              eq = let open ≡-Reasoning in begin
+                    osuc (od→ord x)
+                 ≡⟨ ord-Ord  ⟩
+                    od→ord (Ord (osuc (od→ord x)))
+                 ≡⟨ cong ( λ k → od→ord  k ) ( sym (==→o≡ ( ⇔→==  uxxx-ord ))) ⟩
+                    od→ord (Union (x , (x , x)))
+                 ∎
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
               lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
               lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)