--- a/src/Topology.agda	Tue Feb 21 12:02:41 2023 +0900
+++ b/src/Topology.agda	Wed Feb 22 10:11:00 2023 +0900
@@ -464,10 +464,14 @@
    --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
    --     it means there is a limit
    --
-   Intersection : (X : Ordinal ) →  HOD
-   Intersection X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = ? ; <odmax = ? }
+   Intersection : (X : Ordinal ) → o∅ o< X →  HOD   -- ∩ X
+   Intersection X 0<X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = osuc X ; <odmax = i00 } where
+       i00 : {x : Ordinal} → ({y : Ordinal} → odef (* X) y → odef (* y) x) → x o< osuc X
+       i00 {x} xy = begin
+           x ≤⟨ ? ⟩
+           X ∎ where open o≤-Reasoning O
    has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
-      →  ¬ (  Intersection X  =h= od∅ )
+      →  ¬ (  Intersection X ? =h= od∅ )
    has-intersection {X} CX fip i=0 = ? where
        no-cover : ¬ ( (* (OX CX)) covers L ) 
        no-cover = ?