# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1569197799 -32400
# Node ID 2e75710a936bd4f05eb7258a112551c7675c3a3e
# Parent  53744836020b818adad619682860627fd4ccfaf6
...

diff -r 53744836020b -r 2e75710a936b ordinal.agda
--- a/ordinal.agda	Sun Sep 22 20:26:32 2019 +0900
+++ b/ordinal.agda	Mon Sep 23 09:16:39 2019 +0900
@@ -261,10 +261,10 @@
        caseOSuc lx ox prev = {!!}
 
   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
-  continuum-hyphotheis a x lt = lemma where
-       lemma : Ord (osuc a) ∋ x
-       lemma with IsZF.power→ isZF (Ord a) x lt {{!!}} {!!} 
-       ... | t = {!!}
-
-
-
+  continuum-hyphotheis a x = lemma2 where
+       lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
+       lemma1 = {!!}
+       lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
+       lemma = o<→c< lemma1
+       lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
+       lemma2 = {!!}