--- a/ordinal-definable.agda	Sat Jun 01 14:43:05 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 18:17:24 2019 +0900
@@ -358,14 +358,15 @@
          union-lemma-u {X} {z} U>z = lemma <-osuc where
              lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
              lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
-         union→ :  (X z u : OD) → (Union X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
          union→ X y u xx | tri< a ¬b ¬c = {!!}
-         union→ X y u xx | tri≈ ¬a b ¬c = {!!}
-         union→ X y u xx | tri> ¬a ¬b c = {!!}
-            --  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
+         union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
+             lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
+             lemma refl lt = lt
+         union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
          union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
-         union← X z X∋z = record { proj1 = {!!} ; proj2 = union-lemma-u X∋z }
+         union← X z X∋z = record { proj1 = def-subst {suc n} (o<→c< X∋z) oiso refl ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)