--- a/OD.agda	Fri Jul 03 18:49:05 2020 +0900
+++ b/OD.agda	Fri Jul 03 21:39:10 2020 +0900
@@ -279,7 +279,18 @@
     Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
        ; odmax = osuc (od→ord U) ; <odmax = umax< } where
            umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
-           umax< {y} not = {!!}
+           umax< {y} not = lemma (FExists _ lemma1 not ) where
+               lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
+               lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
+               lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
+               lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
+               lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
+               lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
+               lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
+               lemma not with trio< y (od→ord U)
+               lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
+               lemma not | tri≈ ¬a refl ¬c = <-osuc
+               lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
     _∈_ : ( A B : ZFSet  ) → Set n
     A ∈ B = B ∋ A